package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

A structure S is a non recursive inductive type with a single constructor

type projection = {
  1. proj_name : Names.Name.t;
    (*

    field name

    *)
  2. proj_true : bool;
    (*

    false = projection for a defined field (letin)

    *)
  3. proj_canonical : bool;
    (*

    false = not to be used for CS inference

    *)
  4. proj_body : Names.Constant.t option;
    (*

    the projection function

    *)
}

A projection to a structure field

type t = {
  1. name : Names.inductive;
  2. projections : projection list;
  3. nparams : int;
}
val make : Environ.env -> Names.inductive -> projection list -> t
val register : t -> unit
val subst : Mod_subst.substitution -> t -> t
val rebuild : Environ.env -> t -> t

refreshes nparams, e.g. after section discharging

val find : Names.inductive -> t

find isp returns the Structure.t associated to the inductive path isp if it corresponds to a structure, otherwise it fails with Not_found

val find_from_projection : Names.Constant.t -> t

raise Not_found if not a structure projection

val find_projections : Names.inductive -> Names.Constant.t option list

lookup_projections isp returns the projections associated to the inductive path isp if it corresponds to a structure, otherwise it fails with Not_found

val projection_nparams : Names.Constant.t -> int

raise Not_found if not a projection

val is_projection : Names.Constant.t -> bool
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