search

Soonad / Moonad

An upcoming operating system built on Type-Theory
43 stars 5 forks source link

Incorrect parse on this term #108

Open VictorTaelin opened 4 years ago

VictorTaelin commented 4 years ago

Seems like it parses ?a as part of the type, investigate

T Decision<A: Type>
| Decision.yep(proof: A);
| Decision.nop(proof: Not(A));

Decision.get<A: Type>(dec: Decision(A)): case dec: | A; | Not(A);
  ?a
johnchandlerburnham commented 4 years ago

I this this is happening because parse_cse can take an optional motive. This line: https://github.com/moonad/Formality/blob/1223d71682af9aa60834fcfc282203240e559d3b/javascript/FormalityLang.js#L611 So it reads ?a as the motive instead of the body of the expression.

I'm already working on another issue with parse_cse (as reported bye @emturner on the telegram channel) with parsing extra | branches with parse_bar, so I can work on a solution here too.

emturner commented 4 years ago

does sound similar;

@MaiaVictor asked me to raise an issue for it - it's over at #89 on the Formality repo