max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/interactive): fix tests

Browse source
This commit is contained in:
Gabriel Ebner 2017-07-06 16:32:50 +02:00
parent c7928c16b3
commit f55d10bb50
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/lean/interactive/goal_info_rw.lean.expected.out
View file

@ -1,6 +1,6 @@
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ ((← | <-)? expr), ... ] | (← | <-)? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":3}
{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ ((← | <-)? expr), ... ] | (← | <-)? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":5}
{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":3}
{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":5}
{"record":{"full-id":"h₁","state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = q","type":"p = q"},"response":"ok","seq_num":7}
{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ ((← | <-)? expr), ... ] | (← | <-)? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":8}
{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ ((← | <-)? expr), ... ] | (← | <-)? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":10}
{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":8}
{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | id*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":10}