- -

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.
-