Mercurial > hg > Members > kono > Proof > galois

changeset 56:e26f784cd6b1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 23 Aug 2020 18:07:18 +0900
parents 111c561ae90c
children 518d364a58a3
files Putil.agda
diffstat 1 files changed, 2 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sun Aug 23 17:53:18 2020 +0900
+++ b/Putil.agda	Sun Aug 23 18:07:18 2020 +0900
@@ -132,6 +132,7 @@
 
 open import logic 
 
+-- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] 
 shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (fromℕ n) ≡ fromℕ n → Permutation n n
 shrink {n} perm pn=n  = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
 
@@ -256,7 +257,7 @@
 perm→FL {zero} perm = f0
 perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL ( shrink fl1 {!!} ) where
     fl1 : Permutation (suc n) (suc n)
-    fl1 = perm ∘ₚ pinv ( pins {!!})
+    fl1 = perm ∘ₚ pinv ( pins (fin<n {n} {{!!}}))
     fl1=pprep : perm =p= pprep ( shrink fl1 {!!} )
     fl1=pprep = {!!}