fix

digama0 · Nov 22, 2024 · a26b4f1 · a26b4f1
1 parent 9f917e7
commit a26b4f1
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/examples/compiler.mm0 b/examples/compiler.mm0
@@ -4,6 +4,9 @@ import "x86.mm0";
 -- because it (should) add no new axioms,
 -- but in the interim we are using this to keep the partial proofs checked in CI:
 axiom sorry (p: wff): $ p $;
+term sorry_nat: nat;
+term sorry_set: set;
+term sorry_wff: wff;
 
 -- Search for theorem ... = 'sorry; to find the incomplete proofs
 -- (or delete the sorry axiom and see what breaks). Proofs depending on this axiom