search

sweirich / trellys

Automatically exported from code.google.com/p/trellys
45 stars 6 forks source link

Misc syntactic ugliness #20

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
Feel free to add more ugliness to this issue. E.g. we have both (prog x : Nat) 
and  (x : Nat)=> , we should pick one (perhaps the former?).

Original issue reported on code.google.com by vilhelm....@gmail.com on 4 Jul 2011 at 8:27

GoogleCodeExporter commented 9 years ago 
(Yay, syntax) Is there a way to treat top-level definitions and arrows 
uniformly?  E.g.

  plus :L (L Nat) -> (L Nat)
  div :P (L Nat) -> (L Nat) -> (P Nat)
  append :L (m:L Nat) -> (n:L Nat) -> (L vec m) -> (L vec n) -> (L vec (plus m n))

I guess currently we don't annotate the return-type logicality, because it's 
the logicality of the definition.  So, one of the first or last letter should 
be dropped.

Original comment by nathan.c...@gmail.com on 4 Jul 2011 at 11:41