package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type app_node
val pr_app_node : (EConstr.t -> Pp.t) -> app_node -> Pp.t
type case_stk
type member =
  1. | App of app_node
  2. | Case of case_stk
  3. | Proj of Names.Projection.t
  4. | Fix of EConstr.fixpoint * t
  5. | Primitive of CPrimitives.t * Names.Constant.t * EConstr.EInstance.t * t * CPrimitives.args_red
and t = member list
val pr : (EConstr.t -> Pp.t) -> t -> Pp.t
val empty : t
val is_empty : t -> bool
val compare_shape : t -> t -> bool
exception IncompatibleFold2
val fold2 : ('a -> EConstr.constr -> EConstr.constr -> 'a) -> 'a -> t -> t -> 'a

fold2 f x sk1 sk2 folds f on any pair of term in (sk1,sk2).

  • returns

    the result and the lifts to apply on the terms

val append_app : EConstr.t array -> t -> t

append_app args sk pushes array of arguments args on sk

val append_app_list : EConstr.t list -> t -> t

append_app_list args sk pushes list of arguments args on sk

val strip_app : t -> t * t

if strip_app sk = (sk1,sk2), then sk = sk1 @ sk2 with sk1 purely applicative and sk2 does not start with an argument

val strip_n_app : int -> t -> (t * EConstr.t * t) option
  • returns

    (the nth first elements, the (n+1)th element, the remaining stack) if there enough of those

val decomp_rev : t -> (EConstr.t * t) option

decomp sk extracts the first argument of reversed stack sk is there is some

val not_purely_applicative : t -> bool

not_purely_applicative sk

val list_of_app_stack : t -> EConstr.constr list option

list_of_app_stack sk either returns Some sk turned into a list of arguments if sk is purely applicative and None otherwise

val args_size : t -> int

args_size sk returns the number of arguments available at the head of sk

zip sigma t sk

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