package coq

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

Module TermSource

Derived constructors

non-dependent product t1 -> t2, an alias for forall (_:t1), t2. Beware t_2 is NOT lifted. Eg: in context A:Prop, A->A is built by (mkArrow (mkRel 1) (mkRel 2))

For an always-relevant domain

Named version of the functions from Term.

Constructs either (x:t)c or [x=b:t]c

Constructs either [x:t]c or [x=b:t]c

Other term constructors.

applist (f,args) and its variants work as mkApp

prodn n l b = forall (x_1:T_1)...(x_n:T_n), b where l is (x_n,T_n)...(x_1,T_1)....

compose_prod l b

  • returns

    forall (x_1:T_1)...(x_n:T_n), b where l is (x_n,T_n)...(x_1,T_1). Inverse of decompose_prod.

lamn n l b

  • returns

    fun (x_1:T_1)...(x_n:T_n) => b where l is (x_n,T_n)...(x_1,T_1)....

compose_lam l b

  • returns

    fun (x_1:T_1)...(x_n:T_n) => b where l is (x_n,T_n)...(x_1,T_1). Inverse of it_destLam

Sourceval to_lambda : int -> Constr.constr -> Constr.constr

to_lambda n l

  • returns

    fun (x_1:T_1)...(x_n:T_n) => T where l is forall (x_1:T_1)...(x_n:T_n), T

Sourceval to_prod : int -> Constr.constr -> Constr.constr

to_prod n l

  • returns

    forall (x_1:T_1)...(x_n:T_n), T where l is fun (x_1:T_1)...(x_n:T_n) => T

Sourceval it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
Sourceval it_mkProd_or_LetIn : Constr.types -> Constr.rel_context -> Constr.types
Sourceval lambda_applist : Constr.constr -> Constr.constr list -> Constr.constr

In lambda_applist c args, c is supposed to have the form λΓ.c with Γ without let-in; it returns c with the variables of Γ instantiated by args.

Sourceval lambda_appvect : Constr.constr -> Constr.constr array -> Constr.constr
Sourceval lambda_applist_assum : int -> Constr.constr -> Constr.constr list -> Constr.constr

In lambda_applist_assum n c args, c is supposed to have the form λΓ.c with Γ of length n and possibly with let-ins; it returns c with the assumptions of Γ instantiated by args and the local definitions of Γ expanded.

Sourceval lambda_appvect_assum : int -> Constr.constr -> Constr.constr array -> Constr.constr

pseudo-reduction rule

Sourceval prod_appvect : Constr.types -> Constr.constr array -> Constr.types

prod_appvect forall (x1:B1;...;xn:Bn), B a1...an

  • returns

    B[a1...an]

Sourceval prod_applist : Constr.types -> Constr.constr list -> Constr.types
Sourceval prod_appvect_assum : int -> Constr.types -> Constr.constr array -> Constr.types

In prod_appvect_assum n c args, c is supposed to have the form ∀Γ.c with Γ of length n and possibly with let-ins; it returns c with the assumptions of Γ instantiated by args and the local definitions of Γ expanded.

Sourceval prod_applist_assum : int -> Constr.types -> Constr.constr list -> Constr.types
Other term destructors.

Transforms a product term $ (x_1:T_1)..(x_n:T_n)T $ into the pair $ ((x_n,T_n);...;(x_1,T_1),T) $ , where $ T $ is not a product.

Transforms a lambda term $ x_1:T_1..x_n:T_nT $ into the pair $ ((x_n,T_n);...;(x_1,T_1),T) $ , where $ T $ is not a lambda.

Given a positive integer n, decompose a product term $ (x_1:T_1)..(x_n:T_n)T $ into the pair $ ((xn,Tn);...;(x1,T1),T) $ . Raise a user error if not enough products.

Given a positive integer $ n $ , decompose a lambda term $ x_1:T_1..x_n:T_nT $ into the pair $ ((x_n,T_n);...;(x_1,T_1),T) $ . Raise a user error if not enough lambdas.

Sourceval decompose_prod_assum : Constr.types -> Constr.rel_context * Constr.types

Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let

Idem with lambda's and let's

Sourceval decompose_prod_n_assum : int -> Constr.types -> Constr.rel_context * Constr.types

Idem but extract the first n premisses, counting let-ins.

Sourceval decompose_lam_n_assum : int -> Constr.constr -> Constr.rel_context * Constr.constr

Idem for lambdas, _not_ counting let-ins

Sourceval decompose_lam_n_decls : int -> Constr.constr -> Constr.rel_context * Constr.constr

Idem, counting let-ins

Return the premisses/parameters of a type/term (let-in included)

Sourceval prod_n_assum : int -> Constr.types -> Constr.rel_context

Return the first n-th premisses/parameters of a type (let included and counted)

Sourceval lam_n_assum : int -> Constr.constr -> Constr.rel_context

Return the first n-th premisses/parameters of a term (let included but not counted)

Sourceval strip_prod : Constr.types -> Constr.types

Remove the premisses/parameters of a type/term

Sourceval strip_prod_n : int -> Constr.types -> Constr.types

Remove the first n-th premisses/parameters of a type/term

Sourceval strip_lam_n : int -> Constr.constr -> Constr.constr
Sourceval strip_prod_assum : Constr.types -> Constr.types

Remove the premisses/parameters of a type/term (including let-in)

Sourceval strip_lam_assum : Constr.constr -> Constr.constr
...

An "arity" is a term of the form [x1:T1]...[xn:Tn]s with s a sort. Such a term can canonically be seen as the pair of a context of types and of a sort

Sourceval mkArity : arity -> Constr.types

Build an "arity" from its canonical form

Sourceval destArity : Constr.types -> arity

Destruct an "arity" into its canonical form

Sourceval isArity : Constr.types -> bool

Tell if a term has the form of an arity

Sourcetype sorts_family = Sorts.family =
  1. | InSProp
  2. | InProp
  3. | InSet
  4. | InType
  • deprecated Alias for Sorts.family
Sourcetype sorts = private Sorts.t =
  1. | SProp
  2. | Prop
  3. | Set
  4. | Type of Univ.Universe.t
    (*

    Type

    *)
  • deprecated Alias for Sorts.t
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