package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.0.tar.gz
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

doc/coq-core.kernel/Genlambda/index.html

Module GenlambdaSource

Intermediate language used by both the VM and native.

Sourcetype reloc_table = (int * int) array
Sourcetype '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
Sourceand 'v lam_branches = {
  1. constant_branches : 'v lambda array;
  2. nonconstant_branches : (Names.Name.t Context.binder_annot array * 'v lambda) array;
}
Sourceand 'v fix_decl = Names.Name.t Context.binder_annot array * 'v lambda array * 'v lambda array
Sourcetype evars = {
  1. evars_val : Constr.constr Constr.evar_handler;
}
Sourceval empty_evars : evars
Manipulation functions
Sourceval mkLapp : 'v lambda -> 'v lambda array -> 'v lambda
Sourceval mkLlam : Names.Name.t Context.binder_annot array -> 'v lambda -> 'v lambda
Sourceval decompose_Llam : 'v lambda -> Names.Name.t Context.binder_annot array * 'v lambda
Sourceval decompose_Llam_Llet : 'v lambda -> (Names.Name.t Context.binder_annot * 'v lambda option) array * 'v lambda
Sourceval map_lam_with_binders : (int -> 'a -> 'a) -> ('a -> 'v lambda -> 'v lambda) -> 'a -> 'v lambda -> 'v lambda
Sourceval lam_exlift : Esubst.lift -> 'v lambda -> 'v lambda
Sourceval lam_lift : int -> 'v lambda -> 'v lambda
Sourceval lam_subst_rel : 'v lambda -> Names.Name.t -> int -> 'v lambda Esubst.subs -> 'v lambda
Sourceval lam_exsubst : 'v lambda Esubst.subs -> 'v lambda -> 'v lambda
Sourceval lam_subst_args : 'v lambda Esubst.subs -> 'v lambda array -> 'v lambda array
Sourceval simplify : ('v lambda -> bool) -> 'v lambda Esubst.subs -> 'v lambda -> 'v lambda
Sourceval remove_let : 'v lambda Esubst.subs -> 'v lambda -> 'v lambda
Translation functions
Sourceval make_args : int -> int -> 'v lambda array
Sourceval makeblock : (int -> 'v lambda array -> 'v option) -> Names.inductive -> int -> int -> int -> 'v lambda array -> 'v lambda
Sourceval lambda_of_prim : Environ.env -> Constr.pconstant -> CPrimitives.t -> 'v lambda array -> 'v lambda
Sourcemodule type S = sig ... end
Sourcemodule Make (Val : S) : sig ... end
Printing
Sourceval pp_lam : 'v lambda -> Pp.t