max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/grind_ite_trace.lean.out.expected
Garmelon 08eb78a5b2
chore: switch to new test/bench suite (#12590) 
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.

For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
2026-02-25 13:51:53 +00:00

275 lines
12 KiB
Text
Raw Permalink Blame History

Try these:
[apply]
instantiate only [normalized]
instantiate only [hasNestedIf, hasConstantIf, hasRedundantIf, disjoint]
cases #b01e
· instantiate only [eval]
· instantiate only [vars]
instantiate only [← List.not_mem_nil]
[apply] finish only [normalized, hasNestedIf, hasConstantIf, hasRedundantIf, disjoint, eval, vars, ← List.not_mem_nil,
#b01e]
Try these:
[apply]
instantiate only [= getElem?_pos, normalized]
instantiate only [hasNestedIf, hasConstantIf, hasRedundantIf, disjoint]
cases #a87a
· instantiate only [eval]
instantiate only [= Option.getD_none]
· instantiate only [vars]
instantiate only [= List.mem_cons]
instantiate only [← List.not_mem_nil]
[apply] finish only [= getElem?_pos, normalized, hasNestedIf, hasConstantIf, hasRedundantIf, disjoint, eval,
= Option.getD_none, vars, = List.mem_cons, ← List.not_mem_nil, #a87a]
Try these:
[apply]
instantiate only [= getElem?_neg, = getElem?_pos, normalized]
instantiate only [hasNestedIf, hasConstantIf, hasRedundantIf, disjoint]
cases #b225
· instantiate only [eval]
instantiate only [= Option.getD_some]
· instantiate only [vars]
instantiate only [← List.not_mem_nil]
[apply] finish only [= getElem?_neg, = getElem?_pos, normalized, hasNestedIf, hasConstantIf, hasRedundantIf, disjoint,
eval, = Option.getD_some, vars, ← List.not_mem_nil, #b225]
Try these:
[apply]
instantiate only [#3273, eval]
instantiate only [eval]
[apply] finish only [eval, #3273]
Try these:
[apply]
instantiate only [#3273, eval]
instantiate only [eval]
[apply] finish only [eval, #3273]
Try these:
[apply]
instantiate only [#4b9f, eval]
instantiate only [eval]
cases #9a7f <;> cases #b076 <;> instantiate only [eval]
[apply] finish only [eval, #4b9f, #9a7f, #b076]
Try these:
[apply]
instantiate only [= getElem?_pos]
instantiate only [=_ Std.HashMap.contains_iff_mem]
cases #9125
· instantiate only [#807c, #1ac2, eval]
instantiate only [eval]
cases #c6fb
· cases #c4c1
cases #ad14
·
cases #fe3d <;>
cases #a866 <;>
cases #3b79 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #abae14845457c6e6 <;> instantiate only [= Option.getD_some]
·
cases #2c5b <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #f02f <;>
instantiate only [= Option.getD_some] <;>
cases #fe3d <;> cases #3b79 <;> instantiate only [= Std.HashMap.getElem?_insert] <;> cases #abae
· cases #c4c1
cases #ad14
·
cases #fe3d <;>
cases #a866 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #3b79 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #abae14845457c6e6 <;> cases #f02f <;> instantiate only [= Option.getD_some]
· cases #2c5b
instantiate only [= Std.HashMap.getElem?_insert]
cases #f02f
instantiate only [= Option.getD_some]
cases #fe3d
· cases #a866 <;> instantiate only [= Std.HashMap.getElem?_insert] <;> cases #f02f
·
cases #3b79 <;>
cases #7fad <;> cases #a866 <;> instantiate only [= Std.HashMap.getElem?_insert] <;> cases #f02f
· instantiate only [#c06f]
instantiate only [= Std.HashMap.mem_insert]
[apply] finish only [= getElem?_pos, =_ Std.HashMap.contains_iff_mem, eval, = Std.HashMap.getElem?_insert,
= Option.getD_some, = Std.HashMap.mem_insert, #9125, #807c, #1ac2, #c6fb, #c4c1, #ad14, #fe3d, #a866, #3b79,
#abae14845457c6e6, #2c5b, #f02f, #abae, #7fad, #c06f]
Try these:
[apply]
instantiate only [= getElem?_pos, normalized]
instantiate only [=_ Std.HashMap.contains_iff_mem, hasNestedIf, hasConstantIf, hasRedundantIf, disjoint]
instantiate only [vars, hasConstantIf, hasRedundantIf, disjoint]
instantiate only [List.disjoint]
instantiate only [#e77a, #c06f, List.disjoint]
cases #0dae
· instantiate only [= Std.HashMap.mem_insert]
· cases #88d5
· instantiate only [eval]
instantiate only [eval]
instantiate only [= Option.getD_none]
cases #051b
· instantiate only [#807c]
cases #c4c1 <;>
cases #fe3d <;>
cases #3b79 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #abae <;> instantiate only [= Option.getD_some]
· instantiate only [#1ac2]
cases #c4c1 <;>
cases #7fad <;>
cases #a866 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #f02f <;> instantiate only [= Option.getD_some]
· instantiate only [vars]
instantiate only [= List.mem_append, = List.cons_append]
ac
instantiate only [#c06f, = List.mem_cons]
instantiate only [= Std.HashMap.mem_insert, #e77a]
instantiate only [= Std.HashMap.mem_insert]
[apply] finish only [= getElem?_pos, normalized, =_ Std.HashMap.contains_iff_mem, hasNestedIf, hasConstantIf,
hasRedundantIf, disjoint, vars, List.disjoint, = Std.HashMap.mem_insert, eval, = Option.getD_none,
= Std.HashMap.getElem?_insert, = Option.getD_some, = List.mem_append, = List.cons_append, = List.mem_cons, #e77a,
#c06f, #0dae, #88d5, #051b, #807c, #c4c1, #fe3d, #3b79, #abae, #1ac2, #7fad, #a866, #f02f]
Try these:
[apply]
instantiate only [= getElem?_neg, = getElem?_pos, #4e0f, eval]
instantiate only [eval]
instantiate only [eval, = Option.getD_some]
cases #c6fb
[apply] finish only [= getElem?_neg, = getElem?_pos, eval, = Option.getD_some, #4e0f, #c6fb]
Try these:
[apply]
instantiate only [normalized]
instantiate only [hasNestedIf, hasConstantIf, hasRedundantIf, disjoint]
cases #132b
· instantiate only [eval]
· instantiate only [vars]
instantiate only [← List.not_mem_nil]
[apply] finish only [normalized, hasNestedIf, hasConstantIf, hasRedundantIf, disjoint, eval, vars, ← List.not_mem_nil,
#132b]
Try these:
[apply]
instantiate only [= getElem?_pos, normalized]
instantiate only [=_ Std.HashMap.contains_iff_mem, hasNestedIf, hasConstantIf, hasRedundantIf, disjoint]
cases #190a
· instantiate only [eval]
instantiate only [= Option.getD_none]
· instantiate only [vars]
instantiate only [= List.mem_cons]
instantiate only [← List.not_mem_nil]
[apply] finish only [= getElem?_pos, normalized, =_ Std.HashMap.contains_iff_mem, hasNestedIf, hasConstantIf,
hasRedundantIf, disjoint, eval, = Option.getD_none, vars, = List.mem_cons, ← List.not_mem_nil, #190a]
Try these:
[apply]
instantiate only [= getElem?_neg, = getElem?_pos, normalized]
instantiate only [hasNestedIf, hasConstantIf, hasRedundantIf, disjoint]
cases #d5d4
· instantiate only [eval]
instantiate only [= Option.getD_some]
· instantiate only [vars]
instantiate only [← List.not_mem_nil]
[apply] finish only [= getElem?_neg, = getElem?_pos, normalized, hasNestedIf, hasConstantIf, hasRedundantIf, disjoint,
eval, = Option.getD_some, vars, ← List.not_mem_nil, #d5d4]
Try these:
[apply]
instantiate only [#3273, eval]
instantiate only [eval]
[apply] finish only [eval, #3273]
Try these:
[apply]
instantiate only [#3273, eval]
instantiate only [eval]
[apply] finish only [eval, #3273]
Try these:
[apply]
instantiate only [#4b9f, eval]
instantiate only [eval]
cases #9a7f <;> cases #b076 <;> instantiate only [eval]
[apply] finish only [eval, #4b9f, #9a7f, #b076]
Try these:
[apply]
instantiate only [= getElem?_pos]
instantiate only [=_ Std.HashMap.contains_iff_mem]
cases #8a41
· instantiate only [#807c, #1ac2, eval]
instantiate only [eval]
cases #c6fb
· cases #c4c1
cases #ad14
·
cases #fe3d <;>
cases #a866 <;>
cases #3b79 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #abae14845457c6e6 <;> instantiate only [= Option.getD_some]
·
cases #2c5b <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #f02f <;>
instantiate only [= Option.getD_some] <;>
cases #fe3d <;> cases #3b79 <;> instantiate only [= Std.HashMap.getElem?_insert] <;> cases #abae
· cases #c4c1
cases #ad14
·
cases #fe3d <;>
cases #a866 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #3b79 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #abae14845457c6e6 <;> cases #f02f <;> instantiate only [= Option.getD_some]
· cases #2c5b
instantiate only [= Std.HashMap.getElem?_insert]
cases #f02f
instantiate only [= Option.getD_some]
cases #fe3d
· cases #a866 <;> instantiate only [= Std.HashMap.getElem?_insert] <;> cases #f02f
·
cases #3b79 <;>
cases #7fad <;> cases #a866 <;> instantiate only [= Std.HashMap.getElem?_insert] <;> cases #f02f
· instantiate only [#bad0]
instantiate only [= Std.HashMap.contains_insert]
[apply] finish only [= getElem?_pos, =_ Std.HashMap.contains_iff_mem, eval, = Std.HashMap.getElem?_insert,
= Option.getD_some, = Std.HashMap.contains_insert, #8a41, #807c, #1ac2, #c6fb, #c4c1, #ad14, #fe3d, #a866, #3b79,
#abae14845457c6e6, #2c5b, #f02f, #abae, #7fad, #bad0]
Try these:
[apply]
instantiate only [= getElem?_pos, normalized]
instantiate only [=_ Std.HashMap.contains_iff_mem, hasNestedIf, hasConstantIf, hasRedundantIf, disjoint]
instantiate only [vars, hasConstantIf, hasRedundantIf, disjoint]
instantiate only [List.disjoint]
instantiate only [#a576, #bad0, List.disjoint]
cases #cfda
· instantiate only [= Std.HashMap.contains_insert]
· cases #8360
· instantiate only [eval]
instantiate only [eval]
instantiate only [= Option.getD_none]
cases #051b
· instantiate only [#807c]
cases #c4c1 <;>
cases #fe3d <;>
cases #3b79 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #abae <;> instantiate only [= Option.getD_some]
· instantiate only [#1ac2]
cases #c4c1 <;>
cases #7fad <;>
cases #a866 <;>
instantiate only [= Std.HashMap.getElem?_insert] <;>
cases #f02f <;> instantiate only [= Option.getD_some]
· instantiate only [vars, = Std.HashMap.contains_iff_mem]
instantiate only [= List.mem_append, = List.cons_append]
ac
instantiate only [#bad0, = List.mem_cons]
instantiate only [#a576, = Std.HashMap.contains_insert]
instantiate only [= Std.HashMap.contains_insert]
[apply] finish only [= getElem?_pos, normalized, =_ Std.HashMap.contains_iff_mem, hasNestedIf, hasConstantIf,
hasRedundantIf, disjoint, vars, List.disjoint, = Std.HashMap.contains_insert, eval, = Option.getD_none,
= Std.HashMap.getElem?_insert, = Option.getD_some, = Std.HashMap.contains_iff_mem, = List.mem_append,
= List.cons_append, = List.mem_cons, #a576, #bad0, #cfda, #8360, #051b, #807c, #c4c1, #fe3d, #3b79, #abae, #1ac2,
#7fad, #a866, #f02f]
Try these:
[apply]
instantiate only [= getElem?_neg, = getElem?_pos, #4e0f, eval]
instantiate only [eval]
instantiate only [eval, = Option.getD_some]
cases #c6fb
[apply] finish only [= getElem?_neg, = getElem?_pos, eval, = Option.getD_some, #4e0f, #c6fb]
Reference in a new issue View git blame Copy permalink