Quelle Notations5.out
Sprache: unbekannt
|
|
Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
p 0 0 true
: 0 = 0 /\ true = true
p 0 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
p 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
p 0 0
: forall b : bool, 0 = 0 /\ b = b
p 0 0
: forall b : bool, 0 = 0 /\ b = b
p
: forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
p
: forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
@p nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
@p
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
p 0 0
: forall b : bool, 0 = 0 /\ b = b
p
: forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
p 0 0 true
: 0 = 0 /\ true = true
p 0 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
p 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
p 0 0
: forall b : bool, 0 = 0 /\ b = b
p 0 0
: forall b : bool, 0 = 0 /\ b = b
p
: forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
p
: forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
@p nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
@p
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
f x true
: 0 = 0 /\ true = true
f x
: forall b : bool, 0 = 0 /\ b = b
f x
: forall b : bool, 0 = 0 /\ b = b
@f nat
: forall a1 a2 : nat,
T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
@f
: forall (A : Type) (a1 a2 : A),
T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
x.(f) true
: 0 = 0 /\ true = true
x.(f)
: forall b : bool, 0 = 0 /\ b = b
x.(f)
: forall b : bool, 0 = 0 /\ b = b
@f nat
: forall a1 a2 : nat,
T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
@f
: forall (A : Type) (a1 a2 : A),
T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
: T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
u ?A
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
u ?A
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
u
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
u
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
u nat 0 0 ?B
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
u nat 0 0 bool
: forall b : bool, 0 = 0 /\ b = b
u nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
u nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
u
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
@u
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
@u
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
u
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
u 0 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
u 0 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
@u nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
@u nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
u 0 0 true
: 0 = 0 /\ true = true
u 0 0 true
: 0 = 0 /\ true = true
v
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
v 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
v 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
v 0 true
: 0 = 0 /\ true = true
v
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@v 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
@v 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
v 0
: forall b : bool, 0 = 0 /\ b = b
= ?n@{x:=v 0 (B:=bool)}
: nat
where
?n : [x : forall b : bool, 0 = 0 /\ b = b |- nat]
v
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
v 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
v 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
v 0 true
: 0 = 0 /\ true = true
v
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@v 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
@v 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
v 0
: forall b : bool, 0 = 0 /\ b = b
= ?n@{x:=v 0 (B:=bool)}
: nat
where
?n : [x : forall b : bool, 0 = 0 /\ b = b |- nat]
##
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
##
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## 0 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## 0 0 true
: 0 = 0 /\ true = true
## 0 0 true
: 0 = 0 /\ true = true
## 0 0
: forall b : bool, 0 = 0 /\ b = b
## 0 0
: forall b : bool, 0 = 0 /\ b = b
= ?n@{x:=## 0 0 (B:=bool)}
: nat
where
?n : [x : forall b : bool, 0 = 0 /\ b = b |- nat]
## ?A
: forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
##
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
##
: forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
## nat 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## nat 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## nat 0 0
: forall (B : Type) (b : B), 0 = 0 /\ b = b
## nat 0 0 ?B
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## nat 0 0 ?B
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## nat 0 0 bool
: forall b : bool, 0 = 0 /\ b = b
## nat 0 0 bool true
: 0 = 0 /\ true = true
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## 0 0
: forall b : bool, 0 = 0 /\ b = b
## 0 0
: forall b : bool, 0 = 0 /\ b = b
= ?n@{x:=## 0 0 (B:=bool)}
: nat
where
?n : [x : forall b : bool, 0 = 0 /\ b = b |- nat]
## 0 0 true
: 0 = 0 /\ true = true
## 0 0 true
: 0 = 0 /\ true = true
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0
: forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0 0
: forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## 0 0
: forall b : bool, 0 = 0 /\ b = b
## 0 0
: forall b : bool, 0 = 0 /\ b = b
= ?n@{x:=## 0 0 (B:=bool)}
: nat
where
?n : [x : forall b : bool, 0 = 0 /\ b = b |- nat]
## 0 0 true
: 0 = 0 /\ true = true
## 0 0 true
: 0 = 0 /\ true = true
# 0 0 bool 0%bool
: T
fun a : T => match a with
| # 0 0 _ _ => 1
| _ => 2
end
: T -> nat
#' 0 0 0%bool
: T
fun a : T => match a with
| #' 0 0 _ => 1
| _ => 2
end
: T -> nat
## 0 0 0%bool
: T
fun a : T => match a with
| ## 0 0 _ => 1
| _ => 2
end
: T -> nat
##' 0 0 0%bool
: T
fun a : T => match a with
| ##' 0 0 _ => 1
| _ => 2
end
: T -> nat
P 0 0 bool 0%bool
: T
fun a : T => match a with
| P 0 0 _ _ => 1
| _ => 2
end
: T -> nat
P' 0 0 0%bool
: T
fun a : T => match a with
| P' 0 0 _ => 1
| _ => 2
end
: T -> nat
Q 0 0 0%bool
: T
fun a : T => match a with
| Q 0 0 _ => 1
| _ => 2
end
: T -> nat
Q' 0 0 0%bool
: T
fun a : T => match a with
| Q' 0 0 _ => 1
| _ => 2
end
: T -> nat
Nat.add 0 0
: nat
File "./output/Notations5.v", line 415, characters 13-14:
The command has indeed failed with message:
The term "0" has type "nat" while it is expected to have type "Type".
File "./output/Notations5.v", line 418, characters 13-18:
The command has indeed failed with message:
Unknown interpretation for notation "_ + _".
Some 0
: option nat
File "./output/Notations5.v", line 425, characters 13-14:
The command has indeed failed with message:
The reference f was not found in the current environment.
0 + 0
: nat
0 + 0
: nat
Nat.add 0 0
: nat
File "./output/Notations5.v", line 438, characters 13-18:
The command has indeed failed with message:
Unknown interpretation for notation "_ + _".
[ Dauer der Verarbeitung: 0.67 Sekunden
]
|
2026-03-28
|
