Module Term

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

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

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

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

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.

In lambda_applist_decls 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.

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

• returns

  B[a1...an]

In prod_appvect_decls 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.

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.

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

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

Idem but extracting simultaneously the first n premisses, counting let-ins, in a term and its type.

Idem for lambdas, including let-ins but _not_ counting them; This is typically the function to use to extract the context of a Fix up to and including the decreasing argument, counting as many lambda's as given by the decreasing index + 1

Idem, counting let-ins

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

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

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

Remove the premisses/parameters of a type/term

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

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

Build an "arity" from its canonical form

Destruct an "arity" into its canonical form

Tell if a term has the form of an arity