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

test(tests/lean/run/blast_cc_heq8): new congruence closure procedure can also handle subtypes without using a flattening preprocessing step

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-11 16:50:03 -08:00
parent b40f0ffe8b
commit d736376a6f
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
tests/lean/run/blast_cc_heq8.lean Normal file
View file

@ -0,0 +1,10 @@
open nat subtype
definition f (x : nat) (y : {n : nat | n > x}) : nat :=
x + elt_of y
set_option blast.subst false
example (h : nat → nat) (a b c d : nat) (Ha : h c > h a) (Hb : h d > h b)
: h a = h b → c = d → f (h a) (tag (h c) Ha) = f (h b) (tag (h d) Hb) :=
by inst_simp