package coq

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

This module represents contexts that can capture non-anonymous variables. Individual declarations are then designated by the identifiers they bind.

module Declaration : sig ... end

Representation of local declarations.

type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list

Named-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 named-context

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

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

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

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

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

Return a declaration designated by an identifier of the variable bound in that declaration.

  • raises Not_found

    if the designated identifier is not bound in a given named-context.

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

Check whether given two named-contexts are equal.

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

Map all terms in a given named-context.

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

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

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

Reduce all terms in a given named-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 named-context to a single value. Outermost declarations are processed first.

val to_vars : ('c, 't) pt -> Names.Id.Set.t

Return the set of all identifiers bound in a given named-context.

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

Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

val to_instance : (Names.Id.t -> 'r) -> ('c, 't) pt -> 'r list

to_instance Ω builds an instance args such that Ω ⊢ args:Ω where Ω is a named-context and with the local definitions of Ω skipped. Example: for id1:T,id2:=c,id3:U, it gives Var id1, Var id3. All idj are supposed distinct.

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