test(tests/lean/run): add more tests
This commit is contained in:
parent
d1fa547335
commit
dc203b28db
1 changed files with 16 additions and 0 deletions
16
tests/lean/run/app_builder4.lean
Normal file
16
tests/lean/run/app_builder4.lean
Normal file
|
@ -0,0 +1,16 @@
|
||||||
|
import data.list
|
||||||
|
|
||||||
|
constants f : nat → nat → nat
|
||||||
|
constants a b : nat
|
||||||
|
axiom H2 : a = b
|
||||||
|
set_option pp.all true
|
||||||
|
|
||||||
|
#app_builder congr (eq.refl (f a)), H2
|
||||||
|
|
||||||
|
constants g : ∀ {A :Type}, A → A → A
|
||||||
|
variables A : Type
|
||||||
|
variables l₁ l₂ l₃: list A
|
||||||
|
variables H : l₂ = l₃
|
||||||
|
|
||||||
|
#app_builder congr (eq.refl (g l₁)), H
|
||||||
|
#app_builder congr_arg (g l₁), H
|
Loading…
Reference in a new issue