Quellcode-Bibliothek Cases.out
Sprache: unbekannt
|
|
Columbo aufrufen.out Download desUnknown {[0] [0] [0]}Datei anzeigen
t_rect =
fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
fix F (t : t) : P t :=
match t as t0 return (P t0) with
| k _ x0 => f x0 (F x0)
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
Arguments t_rect (P f)%_function_scope t
= fun d : TT => match d with
| {| f3 := b |} => b
end
: TT -> 0 = 0
= fun d : TT => match d with
| {| f3 := b |} => b
end
: TT -> 0 = 0
proj =
fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
match eq_nat_dec x y with
| left eqprf => match eqprf in (_ = z) return (P z) with
| eq_refl => def
end
| right _ => prf
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
Arguments proj (x y)%_nat_scope P%_function_scope def prf
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
match l with
| nil => None
| (x0 :: nil)%list => Some x0
| (x0 :: (_ :: _) as l0)%list => foo A l0
end
: forall A : Type, list A -> option A
Arguments foo A%_type_scope l%_list_scope
uncast =
fun (A : Type) (x : I A) => match x with
| x0 <: _ => x0
end
: forall A : Type, I A -> A
Arguments uncast A%_type_scope x
foo' = if A 0 then true else false
: bool
f =
fun H : B =>
match H with
| AC x =>
(fun x0 : P b =>
let b0 := b in
(if b0 as b return (P b -> True)
then fun _ : P true => Logic.I
else fun _ : P false => Logic.I) x0) x
end
: B -> True
File "./output/Cases.v", line 91, characters 0-98:
The command has indeed failed with message:
Non exhaustive pattern-matching: no clause found for pattern
gadtTy _ _
File "./output/Cases.v", line 108, characters 17-18:
The command has indeed failed with message:
In environment
texpDenote : forall t : type, texp t -> typeDenote t
t : type
e : texp t
n : nat
The term "n" has type "nat" while it is expected to have type
"typeDenote ?t@{t1:=Nat}".
fun '{{n, m, _}} => n + m
: J -> nat
fun '{{n, m, p}} => n + m + p
: J -> nat
fun '(D n m p q) => n + m + p + q
: J -> nat
File "./output/Cases.v", line 126, characters 29-42:
The command has indeed failed with message:
Once notations are expanded, the resulting constructor D (in type J) is
expected to be applied to no arguments while it is actually applied to
1 argument.
lem1 =
fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
: forall k : nat * nat, k = k
Arguments lem1 k
lem2 =
fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
: forall k : bool, k = k
Arguments lem2 k%_bool_scope
lem3 =
fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
: forall k : nat * nat, k = k
Arguments lem3 k
1 goal
x : nat
n, n0 := match x + 0 with
| 0 | S _ => 0
end : nat
e, e0 :=
match x + 0 as y return (y = y) with
| 0 => eq_refl
| S n => eq_refl
end : x + 0 = x + 0
n1, n2 := match x with
| 0 | S _ => 0
end : nat
e1, e2 := match x return (x = x) with
| 0 => eq_refl
| S n => eq_refl
end
: x = x
============================
x + 0 = 0
1 goal
p : nat
a, a0 :=
match eq_refl as y in (_ = e) return (y = y /\ e = e) with
| eq_refl => conj eq_refl eq_refl
end : eq_refl = eq_refl /\ p = p
a1, a2 :=
match eq_refl in (_ = e) return (p = p /\ e = e) with
| eq_refl => conj eq_refl eq_refl
end : p = p /\ p = p
============================
eq_refl = eq_refl
fun x : comparison => match x with
| Eq => 1
| _ => 0
end
: comparison -> nat
fun x : comparison => match x with
| Eq => 1
| Lt => 0
| Gt => 0
end
: comparison -> nat
fun x : comparison => match x with
| Eq => 1
| Lt | Gt => 0
end
: comparison -> nat
fun x : comparison =>
match x return nat with
| Eq => S O
| Lt => O
| Gt => O
end
: forall _ : comparison, nat
fun x : K => match x with
| a3 | a4 => 3
| _ => 2
end
: K -> nat
fun x : K => match x with
| a1 | a2 => 4
| a3 => 3
| _ => 2
end
: K -> nat
fun x : K => match x with
| a1 | a2 => 4
| a4 => 3
| _ => 2
end
: K -> nat
fun x : K => match x with
| a1 | a3 | a4 => 3
| _ => 2
end
: K -> nat
File "./output/Cases.v", line 224, characters 38-86:
The command has indeed failed with message:
Pattern "S _, _" is redundant in this clause.
stray =
fun N : Tree =>
match N with
| App (App Node (Node as strayvariable)) _ |
App (App Node (App Node _ as strayvariable)) _ |
App (App Node (App (App Node Node) (App _ _) as strayvariable)) _ |
App (App Node (App (App Node (App _ _)) _ as strayvariable)) _ |
App (App Node (App (App (App _ _) _) _ as strayvariable)) _ =>
strayvariable
| _ => Node
end
: Tree -> Tree
Arguments stray N
File "./output/Cases.v", line 253, characters 4-5:
Warning: Unused variable B might be a misspelled constructor. Use _ or _B to
silence this warning. [unused-pattern-matching-variable,default]
File "./output/Cases.v", line 266, characters 33-40:
The command has indeed failed with message:
Application of arguments to a recursive notation not supported in patterns.
File "./output/Cases.v", line 267, characters 33-43:
The command has indeed failed with message:
The constructor cons (in type list) is expected to be applied to 2 arguments
while it is actually applied to 3 arguments.
File "./output/Cases.v", line 268, characters 33-39:
The command has indeed failed with message:
The constructor cons (in type list) is expected to be applied to 2 arguments
while it is actually applied to 1 argument.
File "./output/Cases.v", line 271, characters 33-45:
The command has indeed failed with message:
The constructor D' (in type J') is expected to be applied to 4 arguments (or
6 arguments when including variables for local definitions) while it is
actually applied to 5 arguments.
fun x : J' bool (true, true) =>
match x with
| D' _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
end
: J' bool (true, true) -> {x : nat & x = x}
fun x : J' bool (true, true) =>
match x with
| @D' _ _ _ _ n _ p _ => n + p
end
: J' bool (true, true) -> nat
File "./output/Cases.v", line 277, characters 33-40:
The command has indeed failed with message:
Application of arguments to a recursive notation not supported in patterns.
File "./output/Cases.v", line 278, characters 33-43:
The command has indeed failed with message:
The constructor cons (in type list) is expected to be applied to 2 arguments
while it is actually applied to 3 arguments.
File "./output/Cases.v", line 279, characters 33-39:
The command has indeed failed with message:
The constructor cons (in type list) is expected to be applied to 2 arguments
while it is actually applied to 1 argument.
File "./output/Cases.v", line 281, characters 33-39:
The command has indeed failed with message:
The constructor D' (in type J') is expected to be applied to 3 arguments (or
4 arguments when including variables for local definitions) while it is
actually applied to 2 arguments.
File "./output/Cases.v", line 282, characters 33-45:
The command has indeed failed with message:
The constructor D' (in type J') is expected to be applied to 3 arguments (or
4 arguments when including variables for local definitions) while it is
actually applied to 5 arguments.
fun x : J' bool (true, true) =>
match x with
| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
end
: J' bool (true, true) -> {x : nat & x = x}
fun x : J' bool (true, true) =>
match x with
| @D' _ _ _ _ n _ p _ => (n, p)
end
: J' bool (true, true) -> nat * nat
File "./output/Cases.v", line 313, characters 3-4:
Warning: Unused variable x might be a misspelled constructor. Use _ or _x to
silence this warning. [unused-pattern-matching-variable,default]
File "./output/Cases.v", line 314, characters 6-7:
Warning: Unused variable y might be a misspelled constructor. Use _ or _y to
silence this warning. [unused-pattern-matching-variable,default]
File "./output/Cases.v", line 314, characters 3-4:
Warning: Unused variable x might be a misspelled constructor. Use _ or _x to
silence this warning. [unused-pattern-matching-variable,default]
File "./output/Cases.v", line 325, characters 4-12:
The command has indeed failed with message:
Once notations are expanded, the resulting constructor true (in type bool) is
expected to be applied to no arguments while it is actually applied to
2 arguments.
[ 0.104Quellennavigators
]
|
2026-03-28
|
