Library Beroal.FunListArg
Functions with variable number of arguments
non-dependent type of a function with arbitrary number and types of arguments
Definition type (r : Type)
:= fix rec (args : list Type) : Type
:= match args with
| nil => r
| arg :: argss => arg -> rec argss
end.
:= fix rec (args : list Type) : Type
:= match args with
| nil => r
| arg :: argss => arg -> rec argss
end.
either:
- add ignored last argument;
- generalized axiom K of combinatory logic;
- weakening in sequent calculus.
either:
- add a copy of the last argument as the first argument;
- generalized axiom S of combinatory logic;
- contraction in sequent calculus.
Definition contraction (a b : Type) (xs : list Type)
: (b -> type (b -> a) xs) -> (type (b -> a) xs).
: (b -> type (b -> a) xs) -> (type (b -> a) xs).
move the last argument to the begining
Definition rotate (a b : Type) (xs : list Type)
: Init.iff_Type (type (a -> b) xs) (a -> type b xs).
: Init.iff_Type (type (a -> b) xs) (a -> type b xs).
pointwise operation
Definition pw a0 a1 b n (op : type b (Stream.replicate n a0))
: type (a1 -> b) (Stream.replicate n (a1 -> a0)).
: type (a1 -> b) (Stream.replicate n (a1 -> a0)).