Mercurial > hg > Members > kono > Proof > galois

changeset 59:afa989a4b7e9

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 20:39:35 +0900
parents 80d61b6776d3
children 48926e810f5f
files Putil.agda
diffstat 1 files changed, 10 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/Putil.agda	Sun Aug 23 20:07:23 2020 +0900
+++ b/Putil.agda	Sun Aug 23 20:39:35 2020 +0900
@@ -26,6 +26,16 @@
 
 -- An inductive construction of permutation
 
+-- Todo
+--
+--   complete perm→FL
+--   describe property of pprep and pswap
+--   describe property of pins    ( move 0 to any position)
+--   describe property of shrink  ( remove one column )
+--   prove FL→iso 
+--   prove FL←iso 
+--   prove FL enumerate all permutations
+
 -- we already have refl and trans in the Symmetric Group
 
 pprep  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)