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

test: add new subst tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-23 05:39:25 -07:00
parent 1cb2bd233c
commit a7116b44c1
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/subst.lean
View file

@ -17,6 +17,12 @@ h ▸ rfl
theorem ex3 {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
h₂ ▸ h₁
theorem ex3b {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
h₂.symm ▸ h₁
theorem ex3c {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) : r a c :=
h₂.symm.symm ▸ h₁
theorem ex4 {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) : r a c :=
h₁ ▸ h₂