package coq-core

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

Intermediate language used by both the VM and native.

type reloc_table = (int * int) array
type 'v lambda =
  1. | Lrel of Names.Name.t * int
  2. | Lvar of Names.Id.t
  3. | Levar of Evar.t * 'v lambda array
  4. | Lprod of 'v lambda * 'v lambda
  5. | Llam of Names.Name.t Context.binder_annot array * 'v lambda
  6. | Llet of Names.Name.t Context.binder_annot * 'v lambda * 'v lambda
  7. | Lapp of 'v lambda * 'v lambda array
  8. | Lconst of Constr.pconstant
  9. | Lproj of Names.Projection.Repr.t * 'v lambda
  10. | Lprim of Constr.pconstant * CPrimitives.t * 'v lambda array
  11. | Lcase of case_annot * 'v lambda * 'v lambda * 'v lam_branches
  12. | Lfix of int array * Names.inductive array * int * 'v fix_decl
  13. | Lcofix of int * 'v fix_decl
  14. | Lint of int
  15. | Lparray of 'v lambda array * 'v lambda
  16. | Lmakeblock of Names.inductive * int * 'v lambda array
  17. | Luint of Uint63.t
  18. | Lfloat of Float64.t
  19. | Lval of 'v
  20. | Lsort of Sorts.t
  21. | Lind of Constr.pinductive
  22. | Lforce
and 'v lam_branches = {
  1. constant_branches : 'v lambda array;
  2. nonconstant_branches : (Names.Name.t Context.binder_annot array * 'v lambda) array;
}
and 'v fix_decl = Names.Name.t Context.binder_annot array * 'v lambda array * 'v lambda array
type evars = {
  1. evars_val : Constr.constr CClosure.evar_handler;
}
val empty_evars : Environ.env -> evars
Manipulation functions
val mkLapp : 'v lambda -> 'v lambda array -> 'v lambda
val mkLlam : Names.Name.t Context.binder_annot array -> 'v lambda -> 'v lambda
val decompose_Llam : 'v lambda -> Names.Name.t Context.binder_annot array * 'v lambda
val decompose_Llam_Llet : 'v lambda -> (Names.Name.t Context.binder_annot * 'v lambda option) array * 'v lambda
val map_lam_with_binders : (int -> 'a -> 'a) -> ('a -> 'v lambda -> 'v lambda) -> 'a -> 'v lambda -> 'v lambda
val lam_exlift : Esubst.lift -> 'v lambda -> 'v lambda
val lam_lift : int -> 'v lambda -> 'v lambda
val lam_subst_rel : 'v lambda -> Names.Name.t -> int -> 'v lambda Esubst.subs -> 'v lambda
val lam_exsubst : 'v lambda Esubst.subs -> 'v lambda -> 'v lambda
val lam_subst_args : 'v lambda Esubst.subs -> 'v lambda array -> 'v lambda array
val simplify : ('v lambda -> bool) -> 'v lambda Esubst.subs -> 'v lambda -> 'v lambda
val remove_let : 'v lambda Esubst.subs -> 'v lambda -> 'v lambda
Translation functions
val make_args : int -> int -> 'v lambda array
val makeblock : (int -> 'v lambda array -> 'v option) -> Names.inductive -> int -> int -> int -> 'v lambda array -> 'v lambda
val lambda_of_prim : Environ.env -> Constr.pconstant -> CPrimitives.t -> 'v lambda array -> 'v lambda
module type S = sig ... end
module Make (Val : S) : sig ... end
Printing
val pp_lam : 'v lambda -> Pp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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