test HB.instance with parameters (only in a section)

math-comp · Jun 2, 2020 · 2dc9555 · 2dc9555
1 parent 996e8ed
commit 2dc9555
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/demo4/hierarchy_0.v b/demo4/hierarchy_0.v
@@ -9,6 +9,15 @@ HB.structure Definition s1 T := { A of m1 T A }.
 Check inhab.
   (* inhab : forall (T : Type) (A : s1.type T), s1.sort A *)
 
+HB.instance Definition nat_m1 := m1.Build bool nat 7 false.
+Check (refl_equal _ : @inhab _ _ = 7).
+
+Section Foo.
+Variable A : Type.
+HB.instance Definition list_m1 := m1.Build (option A) (list nat) (cons 7 nil) None.
+End Foo.
+Check (refl_equal _ : @inhab _ _ = (cons 7 nil)).
+
 HB.mixin Record m2 (T : Type) (A : Type) of m1 T A := {
   inj : T -> A;
 }.