Mercurial > hg > Members > kono > Proof > galois

comparison Putil.agda @ 75:4b17a4daf2df

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
3rot
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Aug 2020 00:53:33 +0900
parents 69ed81f8e212
children b0c344ece453
comparison
equal deleted inserted replaced
74:69ed81f8e212 75:4b17a4daf2df
311 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n)) 311 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n))
312 pls6 zero = pid ∷ [] 312 pls6 zero = pid ∷ []
313 pls6 (suc n) = pls5 (suc n) (rev (pls6 n) ) [] -- rev to put id first 313 pls6 (suc n) = pls5 (suc n) (rev (pls6 n) ) [] -- rev to put id first
314 314
315 pls : (n : ℕ ) → List (List ℕ ) 315 pls : (n : ℕ ) → List (List ℕ )
316 pls n = Data.List.map plist (all-perm n) where 316 pls n = Data.List.map plist (all-perm n)