Module Structures.CanonicalSolution
The canonical solution of a problem (proj,val) is a global constant = fun abs : abstractions_ty => body
and body = RecodConstructor params canon_values
and the canonical value corresponding to val is val cvalue_arguments
. It is possible that val is one of the abs
abstractions, eg Default_cs
, and in that case cvalue_abstraction = Some i
type t
=
{
constant : EConstr.t;
abstractions_ty : EConstr.t list;
body : EConstr.t;
nparams : int;
params : EConstr.t list;
cvalue_abstraction : int option;
cvalue_arguments : EConstr.t list;
}
val find : Environ.env -> Evd.evar_map -> (Names.GlobRef.t * ValuePattern.t) -> Evd.evar_map * t
find (p,v)
returns a s such that p s = v. The solution s gets a fresh universe instance and is decomposed into bits for consumption by evarconv. Can raiseNot_found
on failure
val is_open_canonical_projection : Environ.env -> Evd.evar_map -> EConstr.t -> bool
is_open_canonical_projection env sigma t
is true if t is a FieldName applied to term which is not a constructor. Used by evarconv not to unfold too much and lose a projection too early