Merge pull request #16 from dranov/exists-nat

Fix existentially quantified `Nat`s
leanprover-community · Feb 15, 2024 · e0e3d67 · e0e3d67
2 parents a026f4a + b42ec77
commit e0e3d67
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean
@@ -297,7 +297,8 @@ def lamQuantified2STerm (forall? : Bool) (s : LamSort) (body : TransM LamAtom ST
   let dname ← disposableName
   let mut body' ← body
   if s == .base .nat then
-    body' := .qStrApp "=>" #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body']
+    let connective := if forall? then "=>" else "and"
+    body' := .qStrApp connective #[.qStrApp ">=" #[.bvar 0, .sConst (.num 0)], body']
   match forall? with
   | true => return .forallE dname s' body'
   | false => return .existE dname s' body'