Skip to content
This repository was archived by the owner on Aug 24, 2024. It is now read-only.

Commit 98528b3

Browse files
committed
fix: update Dep.lean expected output
1 parent 4e2f41d commit 98528b3

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

test/dep/Dep.lean.leanInk.expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
[{"contents":
2-
"import Mathlib.Tactic.Basic\n\nset_option trace.Elab.info true\n\nexample : ∀ a b : Nat, a = b → b = a := by\n ",
2+
"import Mathlib.Tactic.Basic\n\nexample : ∀ a b : Nat, a = b → b = a := by\n ",
33
"_type": "text"},
44
{"messages": [],
55
"goals":

0 commit comments

Comments
 (0)