From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- .../mathcomp.test_suite.hierarchy_test.html | 76 ++++++++++++++++++++++ 1 file changed, 76 insertions(+) create mode 100644 docs/htmldoc/mathcomp.test_suite.hierarchy_test.html (limited to 'docs/htmldoc/mathcomp.test_suite.hierarchy_test.html') diff --git a/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html b/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html new file mode 100644 index 0000000..1fd348f --- /dev/null +++ b/docs/htmldoc/mathcomp.test_suite.hierarchy_test.html @@ -0,0 +1,76 @@ + + + + + +mathcomp.test_suite.hierarchy_test + + + + +
+ + + +
+ +

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.
+
+
+ + + +
+ + + \ No newline at end of file -- cgit v1.2.3