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 in reverse order 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.

  • deprecated [to_instance] was missing a [List.rev] to comply to its specification; rely on [instance] for the correct specification or use [List.rev (instance ...)] for strict compatibility
val instance : (Names.Id.t -> 'r) -> ('c, 't) pt -> 'r array

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

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

instance_list is like instance but returning a list.