Better diagnose syntax problems in inductive definitions with double implications

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

https://hol-theorem-prover.org

Other

606 stars 132 forks source link

Better diagnose syntax problems in inductive definitions with double implications #1213

Closed mrichards30 closed 3 months ago

mrichards30 commented 3 months ago

This PR aims to address issue #1074 by adding an error message when trying to include a double implication in inductive definitions.

mn200 commented 3 months ago

Thanks for this!