Some issue that may interference with my idea on regular enumeration

1. implicte variable in agda, HAHA, actually this is to omit the type declaration for the parameter in dependent type
   
2. find carefully in ocaml haskell agda coq and epigam for it
3. try to figure out a small ML language as our base, or just to invent a new one