search

latte-central / latte-kernel

The (very) small kernel of the LaTTe proof assistant
MIT License
11 stars 4 forks source link

Bugfix in typing? #18

Closed AustenPrinciple closed 4 years ago

AustenPrinciple commented 4 years ago

This really looks like a bug, since having a single-branch if and discarding the result doesn't look like intended behaviour, but that behaviour is validated by a single test. Changing that single test doesn't break anything, and the entire library still works with it. See the first commit (https://github.com/latte-central/latte-kernel/commit/ffe5d1075e512437d86947823f1ebb368f674646) for a simpler view of what changed.

fredokun commented 4 years ago

Yes obviously it's a bug, thx !