package coq

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

Module Reductionops.StackSource

Sourcetype app_node
Sourceval pr_app_node : (EConstr.t -> Pp.t) -> app_node -> Pp.t
Sourcetype case_stk
Sourceand t = member list
Sourceval pr : (EConstr.t -> Pp.t) -> t -> Pp.t
Sourceval empty : t
Sourceval is_empty : t -> bool
Sourceval compare_shape : t -> t -> bool
Sourceexception IncompatibleFold2
Sourceval 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

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

append_app args sk pushes array of arguments args on sk

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

append_app_list args sk pushes list of arguments args on sk

Sourceval 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

Sourceval 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

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

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

Sourceval not_purely_applicative : t -> bool

not_purely_applicative sk

Sourceval 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

Sourceval 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