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 Constr.binder_annot array * 'v lambda
  6. | Llet of Names.Name.t Constr.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. | Lstring of Pstring.t
  20. | Lval of 'v
  21. | Lsort of Sorts.t
  22. | Lind of Constr.pinductive
and 'v lam_branches = {
  1. constant_branches : 'v lambda array;
  2. nonconstant_branches : (Names.Name.t Constr.binder_annot array * 'v lambda) array;
}
and 'v fix_decl = Names.Name.t Constr.binder_annot array * 'v lambda array * 'v lambda array
type evars = {
  1. evars_val : 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 Constr.binder_annot array -> 'v lambda -> 'v lambda
val decompose_Llam : 'v lambda -> Names.Name.t Constr.binder_annot array * 'v lambda
val decompose_Llam_Llet : 'v lambda -> (Names.Name.t Constr.binder_annot * 'v lambda option) array * 'v lambda
val free_rels : 'v lambda -> Int.Set.t
val optimize : 'v lambda -> 'v lambda
Translation functions
val get_alias : Environ.env -> Names.Constant.t -> Names.Constant.t * bool array
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 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