FAQ

Welcome to the hierarchy-builder FAQ

• I'm getting "Error: unable to graft this clause: no clause named compress:begin"

  You need to require HB before other files using it. From HB Require Import structures. should be the first line of every file. (This error should be gone with Coq-Elpi >= 1.10.x)

• "Error: elpi: split-at run out of list items"

  Precise the types of the parameters and possibly add #[key(T)] attribute.

• I'm getting "Error: You must declare the current class indt «axioms_» before indt «Blah.axioms_»"

  You might need to amend your hierarchy with an explicit join. For a concrete illustration, see this issue. See also this dedicated page.

• I'm getting

  Definition illtyped: In environment [...]
  The term "id_phant" has type [...]
  while it is expected to have type
   "unify _ _ [Object] ?t (is_not_canonically_a [Structure])".
  

  It means Coq cannot find a [Structure] instance on [Object]. Here are possible reasons:

  • it is not declared,
  • there is a declaration, but HB did not register it,
  • it is declared and registered, but the containing module/file is not imported,
  • the preconditions for the instance to hold are not fulfilled.