package coq

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module CbvSource

Sourcetype cbv_infos

Entry point for cbv normalization of a constr

Sourceval shift_value : int -> cbv_value -> cbv_value
Sourceval stack_app : cbv_value array -> cbv_stack -> cbv_stack
Sourceval strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack

recursive functions...

Sourceval cbv_norm_value : cbv_infos -> cbv_value -> Constr.constr

End of cbv debug section i

OCaml

Innovation. Community. Security.