For whatever reason, the Caledon program will stall, eating up an arbitrarily large amount of memory when encountering certain code which should instead produce syntax errors. Here are some examples of code which, if encountered, will trigger what I'm talking about;
defn unit : prop
as \(P : prop) P . P
defn unit : prop
as [P : prop] P -> P
defn tt : unit
as \0 p . p
defn unit : prop
| tt = \(P : prop) . unit
defn unit : prop
| one = unit
a(
For whatever reason, the Caledon program will stall, eating up an arbitrarily large amount of memory when encountering certain code which should instead produce syntax errors. Here are some examples of code which, if encountered, will trigger what I'm talking about;