declare axioms_ as typeclass

Author: Tragicus

Changelog.md

@@ -12,9 +12,9 @@
 	`T` to `S.type` whenever `T` is not a global type (e.g. a variable). Note
 	that `S.pack` can cast a `t : T` to `S.type` only if an instance of the
 	class `S` on `t` is found by type class inference
-- **Change** `HB.structure` declares the class of a structure (`axioms_`) as a
-	type class on the subject with all arguments in output mode but for the
-	subject that is in input mode.
+- **New** Attribute `#[typeclass]` to declare the class of a
+	structure (`axioms_`) as a type class on the subject with all arguments in
+	output mode but for the subject that is in input mode.
 
 ## [1.7.0] - 2024-01-10
 

HB/structure.elpi

@@ -127,6 +127,11 @@ declare Module BSkel Sort :- std.do! [
     ])
     (coq.say "declare:" ClassName "should be an inductive", fail),
 
+  if (get-option "typeclass" tt) (
+	 coq.TC.declare-class ClassName,
+	 coq.hints.add-mode ClassName "typeclass_instances" {std.append {std.map {std.iota {w-params.nparams MLwP}} (_\ r\ r = mode-output)} [mode-input]})
+	 (true),
+
   if-verbose (coq.say {header} "accumulating various props"),
   std.flatten [
       Factories, [ClassAlias], [is-structure Structure],