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

chore(tests/lean/trace1): fix test

Browse source 
@kha: `trace_root` and `trace_ctx` will probably have to be macros that add
`thunk.mk` for us. The coercion is not applied because the types contain metavariables.
The alternative is to implement a more robust coercion resolution procedure.
This commit is contained in:
Leonardo de Moura 2018-08-21 16:20:13 -07:00
parent 3ab1ebcb3f
commit a968b68942
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/trace1.lean
View file

@ -5,15 +5,15 @@ namespace trace
meta def test (opts : options) : id trace_map :=
prod.snd <$> trace_t.run opts (
trace_root ⟨1, 0⟩ `trace.type_context.is_def_eq "type_context.is_def_eq trace" (
trace_ctx `trace.type_context.is_def_eq "f 0 =?= f a (approximate mode)" (
trace_ctx `trace.type_context.is_def_eq_detail "f 0 =?= f a" (
trace_root ⟨1, 0⟩ `trace.type_context.is_def_eq "type_context.is_def_eq trace" ⟨λ _,
trace_ctx `trace.type_context.is_def_eq "f 0 =?= f a (approximate mode)" ⟨λ _,
trace_ctx `trace.type_context.is_def_eq_detail "f 0 =?= f a" ⟨λ _,
trace `trace.type_context.is_def_eq_detail "0 =?= a" >>
trace `trace.type_context.is_def_eq_detail "...failed"
) >>
⟩ >>
trace `trace.type_context.is_def_eq "...failed"
)
))
⟩
⟩)
run_cmd
do let test opts := tactic.trace $ format.join $ list.intersperse format.line $ (test opts).to_list.map $ λ ⟨pos, tr⟩, to_fmt pos ++ ": " ++ tr.pp,