mzacho / refinement-types

A refinement type checker for simply typed lamda calculus with inductive data-types and well-founded recursive functions
MIT License
0 stars 1 forks source link

parsing: precedence of negation wrt. conj/ disj is wrong #16

Closed mzacho closed 9 months ago

mzacho commented 9 months ago

so the type of lt is currently parsed incorrectly