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

test(tests/lean/run/blast_cc3): add test for congruence_closure with dependent types

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-20 13:53:36 -08:00
parent 8f368cebbf
commit 2627eade8b
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
tests/lean/run/blast_cc3.lean Normal file
View file

@ -0,0 +1,15 @@
open nat
set_option blast.subst false
constant f (a b : nat) : a > b → nat
constant g : nat → nat
definition tst
(a₁ a₂ b₁ b₂ c d : nat)
(H₁ : a₁ > b₁)
(H₂ : a₂ > b₂) :
a₁ = c → a₂ = c →
b₁ = d → d = b₂ →
g (g (f a₁ b₁ H₁)) = g (g (f a₂ b₂ H₂)) :=
by blast
print tst