Minor bug fix in correctType

leanprover-community · Jan 10, 2025 · 35dd124 · 35dd124
1 parent 37a909c
commit 35dd124
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Auto/Parser/SMTParser.lean b/Auto/Parser/SMTParser.lean
@@ -358,7 +358,7 @@ def correctType (e : Expr) (parseTermConstraint : ParseTermConstraint) : MetaM E
   | expectedType t => do
     if ← isDefEq eType t then return e
     else if eType.isProp && (← isDefEq t (mkConst ``Bool)) then whnf $ ← mkAppOptM ``decide #[some e, none]
-    else if (← isDefEq eType (mkConst ``Bool)) && t.isProp then whnf $ ← mkAppM ``eq_true #[e]
+    else if (← isDefEq eType (mkConst ``Bool)) && t.isProp then whnf $ ← mkAppM ``Eq #[e, mkConst ``true]
     else if (← isDefEq eType (mkConst ``Nat)) && (← isDefEq t (mkConst ``Int)) then return ← mkAppM ``Int.ofNat #[e]
     else if (← isDefEq eType (mkConst ``Int)) && (← isDefEq t (mkConst ``Nat)) then return ← mkAppM ``Int.natAbs #[e]
     else throwError "correctType :: {e} is parsed as {eType} which is not a {t}"