package coq

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

Representation of contexts that can capture anonymous as well as non-anonymous variables. Individual declarations are then designated by de Bruijn indexes.

module Declaration : sig ... end
type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list

Rel-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list.

val empty : ('c, 't) pt

empty rel-context

val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt

Return a new rel-context enriched by with a given inner-most declaration.

val length : ('c, 't) pt -> int

Return the number of local declarations in a given rel-context.

val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool

Check whether given two rel-contexts are equal.

val nhyps : ('c, 't) pt -> int

Return the number of local assumptions in a given rel-context.

val lookup : int -> ('c, 't) pt -> ('c, 't) Declaration.pt

Return a declaration designated by a given de Bruijn index.

  • raises Not_found

    if the designated de Bruijn index outside the range.

val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt

Map all terms in a given rel-context.

val iter : ('c -> unit) -> ('c, 'c) pt -> unit

Perform a given action on every declaration in a given rel-context.

val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a

Reduce all terms in a given rel-context to a single value. Innermost declarations are processed first.

val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a

Reduce all terms in a given rel-context to a single value. Outermost declarations are processed first.

val to_tags : ('c, 't) pt -> bool list

Map a given rel-context to a list where each local assumption is mapped to true and each local definition is mapped to false.

val drop_bodies : ('c, 't) pt -> ('c, 't) pt

Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

val to_extended_list : (int -> 'r) -> int -> ('c, 't) pt -> 'r list

extended_list mk n Γ builds an instance args such that Γ,Δ ⊢ args:Γ with n = |Δ| and with the local definitions of Γ skipped in args where mk is used to build the corresponding variables. Example: for x:T, y:=c, z:U and n=2, it gives mk 5, mk 3.

val to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array

extended_vect n Γ does the same, returning instead an array.

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