LS-Lab / KeYmaeraX-release

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
http://keymaeraX.org/
GNU General Public License v2.0
76 stars 38 forks source link

Some syntax errors only found upon starting proof #95

Closed rbohrer closed 2 years ago

rbohrer commented 2 years ago

To reproduce, attempt upload just the broken model from issue #93, not both models. If you do that, it will upload successfully, but then when you go to "Start Proof" it will finally give you the error message about the missing variable declaration.

Instead I would expect all the syntax errors on the model editor page

smitsch commented 2 years ago

See #94