small fix

leanprover-community · Feb 16, 2024 · b9f4ce2 · b9f4ce2
1 parent abbe4b3
commit b9f4ce2
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 6 deletions.
diff --git a/Test/LamEmbed.lean b/Test/LamEmbed.lean
@@ -15,8 +15,9 @@ def manyArgFuncTy (n : Nat) (k : Nat) : LamSort :=
 set_option maxRecDepth 4000 in
 set_option lazyReduce.logInfo false in
 #lazyReduce manyArgFuncTy 3000 0
+
 set_option maxRecDepth 2000 in
-#reduce LamSort.beq_eq (manyArgFuncTy 100 40) (manyArgFuncTy 100 40)
+#reduce @LamSort.eq_of_beq_eq_true (manyArgFuncTy 100 40) (manyArgFuncTy 100 40)
 
 -- λ (x₁ x₂ ... xₙ : (.atom 0)) . (.atom 0) x₁ x₂ ... xₙ
 -- Note that the first `.atom 0` is a type atom, while the
@@ -76,6 +77,3 @@ set_option maxHeartbeats 20000000 in
 set_option lazyReduce.printTime true
 set_option maxRecDepth 50000 in
 #lazyReduce List.map (fun n => (List.range (1000 + n)).length) (List.range 10)
-
-set_option maxRecDepth 50000 in
-#lazyReduce (List.range 10000).length
diff --git a/Test/SmtTranslation/BoolNatInt.lean b/Test/SmtTranslation/BoolNatInt.lean
@@ -36,5 +36,3 @@ example {a b c d : Bool} (h : if (if (2 < 3) then a else b) then c else d) :
   (a → c) ∧ (¬ a → d) := by auto
 
 example {a : Bool} : decide a = a := by auto
-
-#check Lean.Elab.Command.elabStructure
Original file line number	Diff line number	Diff line change
Expand Up		@@ -36,5 +36,3 @@ example {a b c d : Bool} (h : if (if (2 < 3) then a else b) then c else d) :
		(a → c) ∧ (¬ a → d) := by auto

		example {a : Bool} : decide a = a := by auto

		#check Lean.Elab.Command.elabStructure