google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

42t is accepted at the value level #106

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
... and vica-versa:

prompt> 42t

42t :: Nat' 42t

the suffix should be looked up in the respective namespace, but right now there 
is only one namespace for suffices. This lookup gives us the 'S' and 'Z' 
constructors, but these in turn have a definition in the value level.

Original issue reported on code.google.com by ggr...@gmail.com on 27 Jun 2012 at 11:33