swap = fun '(x, y) => (y, x)
: A * B -> B * A
Arguments swap pat
fun '(x, y) => (y, x)
: A * B -> B * A
forall '(x, y), swap (x, y) = (y, x)
: Prop
proj_informative = fun '(exist _ x _) => x
: {x : A | P x} -> A
Arguments proj_informative pat
foo = fun '(Bar n b tt p) => if b then n + p else n - p
: Foo -> nat
Arguments foo pat
baz =
fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
: Foo -> Foo -> nat
Arguments baz pat pat
swap =
fun (A B : Type) '(x, y) => (y, x)
: forall {A B : Type}, A * B -> B * A
Arguments swap {A B}%_type_scope pat
fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
: forall A B : Type, A * B -> Prop
forall (A B : Type) '(x, y), swap (x, y) = (y, x)
: Prop
exists '(x, y), swap (x, y) = (y, x)
: Prop
exists '(x, y) '(z, w), swap (x, y) = (z, w)
: Prop
fun '(x, y) => (y, x)
: A * B -> B * A
forall '(x, y), swap (x, y) = (y, x)
: Prop
both_z =
fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p)
: forall pat : nat * nat, F pat
Arguments both_z pat
fun '(x, y) '(z, t) => swap (x, y) = (z, t)
: A * B -> B * A -> Prop
forall '(x, y) '(z, t), swap (x, y) = (z, t)
: Prop
fun (pat : nat) '(x, y) => x + y = pat
: nat -> nat * nat -> Prop
f = fun x : nat => x + x
: nat -> nat
Arguments f x%_nat_scope
fun x : nat => x + x
: nat -> nat
[ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
]
