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

fix(tests/lean/simplifier11): contextual ite lemma has been renamed

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-22 17:08:15 -08:00
parent d240b06ba2
commit a0284b0e82
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/simplifier11.lean
View file

@ -43,7 +43,7 @@ constants {b c x y u v : Prop} (dec_b : decidable b) (dec_c : decidable c)
attribute h_t [simp]
attribute h_e [simp]
attribute if_congr_prop [congr]
attribute if_ctx_congr_prop [congr]
#simplify iff env 0 (ite b x y)
end if_congr_prop