search

opencompl / lean-mlir

A minimal development of SSA theory
Other
88 stars 10 forks source link

chore: Add guard messages to automata proof, remove dependence on sorry axiom #579

Closed AtticusKuhn closed 2 months ago

AtticusKuhn commented 2 months ago

This PR add guard_msgs to the automata file. This ensures that none of the test cases accidentally depend on the sorry axiom, thus resulting in unsound proofs.

Any proofs produced by the automata tactic depends on the axioms [propext, Classical.choice, Lean.ofReduceBool, Quot.sound] but not on the sorry axiom.

This PR was particularly important to @bollu .

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)