Skip to content

Commit 964db5b

Browse files
leodemourakim-em
authored andcommitted
chore: move test to run
1 parent dcdd650 commit 964db5b

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

tests/lean/grind/grind_sym_prio.lean renamed to tests/lean/run/grind_sym_prio.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
opaque q : Nat → Prop
22
opaque p : Nat → Prop
33

4+
attribute [grind symbol default] HAdd.hAdd
5+
46
/-- info: foo: [@HAdd.hAdd `[Nat] `[Nat] `[Nat] `[instHAdd] #6 #5] -/
57
#guard_msgs (info) in
68
@[grind? =>] theorem foo (x y : Nat) : x + y < 10 → q x → p x → p y → q y → x = y := by

0 commit comments

Comments
 (0)