fix

FormalMathematicsLab · Sep 5, 2023 · 2115d38 · 2115d38
1 parent 72d20e5
commit 2115d38
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/Logic/Predicate/FirstOrder/Arith/Model.lean b/Logic/Predicate/FirstOrder/Arith/Model.lean
@@ -77,7 +77,7 @@ lemma modelsPeano : ℕ ⊧* Axiom.Peano oRing :=
 
 end standardModel
 
-theorem Peano.IsConsistent : Logic.Proof.Consistent (Axiom.Peano oRing) :=
+theorem Peano.IsConsistent : Logic.System.Consistent (Axiom.Peano oRing) :=
   Logic.Sound.consistent_of_model standardModel.modelsPeano
 
 variable (L : Language.{u}) [L.ORing]

diff --git a/Main.lean b/Main.lean
@@ -1 +1,4 @@
 import «Logic»
+
+unsafe def main : IO Unit :=
+  IO.println s!"0 = 1"