package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val env_nf_evar : Evd.evar_map -> Environ.env -> Environ.env
val env_nf_betaiotaevar : Evd.evar_map -> Environ.env -> Environ.env
type type_constraint = EConstr.types option
type val_constraint = EConstr.constr option
val empty_tycon : type_constraint
val empty_valcon : val_constraint
val mk_valcon : EConstr.constr -> val_constraint

Instantiate an evar by as many lambda's as needed so that its arguments are moved to the evar substitution (i.e. turn ?x[vars1:=args1] args into ?y[vars1:=args1,vars:=args] with vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]

If the constraint can be made to look like array A return A, otherwise return None (this makes later coercion possible).

val valcon_of_tycon : type_constraint -> val_constraint
val lift_tycon : int -> type_constraint -> type_constraint
val define_evar_as_sort : Environ.env -> Evd.evar_map -> EConstr.existential -> Evd.evar_map * Sorts.t
debug pretty-printer:

Used for bidi heuristic when typing lambdas. Transforms an applied evar to an evar with bigger context (ie ?X e to ?X'@y=e).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct