From a26b4f153e93bdbfbb6497926f9bfa33c7cd93e1 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 22 Nov 2024 02:34:55 +0100
Subject: [PATCH] fix

---
 examples/compiler.mm0 | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/examples/compiler.mm0 b/examples/compiler.mm0
index cb900336..99e158fe 100644
--- 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