package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type cbv_infos
and cbv_stack =
  1. | TOP
  2. | APP of cbv_value array * cbv_stack
  3. | CASE of Constr.constr * Constr.constr array * Constr.case_info * cbv_value Esubst.subs * cbv_stack
  4. | PROJ of Names.Projection.t * cbv_stack
val shift_value : int -> cbv_value -> cbv_value
val stack_app : cbv_value array -> cbv_stack -> cbv_stack
val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
val apply_stack : cbv_infos -> Constr.constr -> cbv_stack -> Constr.constr
val cbv_norm_value : cbv_infos -> cbv_value -> Constr.constr
OCaml

Innovation. Community. Security.