Library mathcomp.test_suite.hierarchy_test
Generated by etc/utils/hierarchy_test.py
`check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`.
Tactic Notation "check_join"
open_constr(t1) open_constr(t2) open_constr(tjoin) :=
let T1 := open_constr:(_ : t1) in
let T2 := open_constr:(_ : t2) in
match tt with
| _ ⇒ unify ((id : t1 → Type) T1) ((id : t2 → Type) T2)
| _ ⇒ fail "There is no join of" t1 "and" t2
end;
let Tjoin :=
lazymatch T1 with
| _ (_ ?Tjoin) ⇒ constr: (Tjoin)
| _ ?Tjoin ⇒ constr: (Tjoin)
| ?Tjoin ⇒ constr: (Tjoin)
end
in
is_evar Tjoin;
let tjoin' := type of Tjoin in
lazymatch tjoin' with
| tjoin ⇒ lazymatch tjoin with
| tjoin' ⇒ idtac
| _ ⇒ idtac tjoin'
end
| _ ⇒ fail "The join of" t1 "and" t2 "is" tjoin'
"but is expected to be" tjoin
end.
Goal False.
open_constr(t1) open_constr(t2) open_constr(tjoin) :=
let T1 := open_constr:(_ : t1) in
let T2 := open_constr:(_ : t2) in
match tt with
| _ ⇒ unify ((id : t1 → Type) T1) ((id : t2 → Type) T2)
| _ ⇒ fail "There is no join of" t1 "and" t2
end;
let Tjoin :=
lazymatch T1 with
| _ (_ ?Tjoin) ⇒ constr: (Tjoin)
| _ ?Tjoin ⇒ constr: (Tjoin)
| ?Tjoin ⇒ constr: (Tjoin)
end
in
is_evar Tjoin;
let tjoin' := type of Tjoin in
lazymatch tjoin' with
| tjoin ⇒ lazymatch tjoin with
| tjoin' ⇒ idtac
| _ ⇒ idtac tjoin'
end
| _ ⇒ fail "The join of" t1 "and" t2 "is" tjoin'
"but is expected to be" tjoin
end.
Goal False.