# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598182775 -32400
# Node ID afa989a4b7e991abf5bb33924217ca654ef00e8d
# Parent  80d61b6776d3b38bb5ed8a84c6585b1923a8979e
...

diff -r 80d61b6776d3 -r afa989a4b7e9 Putil.agda
--- 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)