Generalise
Raised when generalisation is not a good idea. Currently when
the type of a particular judgement, ordinal being witnesses or ordinal variables
val recompose : ?general:bool -> Ast.schema -> Ast.term_or_kind particular
function to apply a schema. I
general = false
, it replace the ordinals with appropriate witnesses to prove the schema (not to use it).general = true
, we want to use the schema and all ordinals are replaced with variablesval recompose_kind : ?general:bool -> Ast.schema -> Ast.kind particular
recompose for subtyping
val recompose_term : ?general:bool -> Ast.schema -> unit particular
recompose for typing
val generalise : ?manual:bool -> Ast.ordi list -> Ast.term_or_kind -> Ast.kind -> Sct.t -> (Ast.schema * (int * Ast.ordi) list) option
Returns the list of unification variables. When a variable has arguments, they should be identical for all occurences.