michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/run/simplifier1): option name

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-09 12:30:20 -08:00
parent bed03272f5
commit 50323e5b14
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/simplifier1.lean
View file

@ -5,7 +5,7 @@ constant q : P → nat → Prop
set_option blast.simp false
set_option trace.blast true
set_option trace.congruence_closure true
set_option trace.cc true
example (a : nat) (h₁ h₂ : P) : q h₁ a = q h₂ a :=
by blast