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

fix(tests): move test away from run

Browse source
This commit is contained in:
Gabriel Ebner 2017-05-22 17:51:10 +02:00
parent cb28f382a3
commit fbfec02015
2 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

0
tests/lean/run/eqn_compiler_ctor.lean → tests/lean/eqn_compiler_ctor.lean
View file

1
tests/lean/eqn_compiler_ctor.lean.expected.out Normal file
View file

@ -0,0 +1 @@
eqn_compiler_ctor.lean:10:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)