Impressum Notations.out
Interaktion und
Portierbarkeitunbekannt
|
|
Haftungsausschluß.out KontaktUnknown {[0] [0] [0]}diese Dinge liegen außhalb unserer Verantwortung
true ? 0; 1
: nat
if true as x return (x ? nat; bool) then 0 else true
: nat
fun e : nat * nat => proj1 e
: nat * nat -> nat
decomp (true, true) as t, u in (t, u)
: bool * bool
! (0 = 0)
: Prop
forall n : nat, n = 0
: Prop
! (0 = 0)
: Prop
forall n : nat, # (n = n)
: Prop
forall n n0 : nat, ## (n = n0)
: Prop
forall n n0 : nat, ### (n = n0)
: Prop
[1; 2; 4]
: list nat
(1; 2, 4)
: nat * nat * nat
ifzero 3
: bool
pred 3
: nat
fun n : nat => pred n
: nat -> nat
fun n : nat => pred n
: nat -> nat
fun x : nat => ifn x is succ n then n else 0
: nat -> nat
1 -
: bool
File "./output/Notations.v", line 97, characters 46-62:
The command has indeed failed with message:
Cannot find where the recursive pattern starts.
File "./output/Notations.v", line 100, characters 0-58:
The command has indeed failed with message:
in the right-hand side, y and z should appear in
term position as part of a recursive pattern.
File "./output/Notations.v", line 103, characters 57-58:
The command has indeed failed with message:
The reference w was not found in the current environment.
File "./output/Notations.v", line 109, characters 0-78:
The command has indeed failed with message:
in the right-hand side, y and z should appear in
term position as part of a recursive pattern.
File "./output/Notations.v", line 110, characters 56-57:
The command has indeed failed with message:
z is expected to occur in binding position in the right-hand side.
File "./output/Notations.v", line 114, characters 0-102:
The command has indeed failed with message:
as y is a non-closed binder, no such "," is allowed to occur.
File "./output/Notations.v", line 118, characters 46-69:
The command has indeed failed with message:
Cannot find where the recursive pattern starts.
File "./output/Notations.v", line 119, characters 46-62:
The command has indeed failed with message:
Cannot find where the recursive pattern starts.
File "./output/Notations.v", line 120, characters 49-63:
The command has indeed failed with message:
Cannot find where the recursive pattern starts.
File "./output/Notations.v", line 121, characters 50-64:
The command has indeed failed with message:
Cannot find where the recursive pattern starts.
File "./output/Notations.v", line 124, characters 0-73:
The command has indeed failed with message:
Both ends of the recursive pattern are the same.
SUM (nat * nat) nat
: Set
FST (0; 1)
: nat
Nil
: forall A : Type, list A
NIL : list nat
: list nat
(false && I 3)%bool /\ I 6
: Prop
[|1, 2, 3; 4, 5, 6|]
: nat * nat * nat * (nat * nat * nat)
File "./output/Notations.v", line 167, characters 0-210:
Warning: Notations "[| _ , _ , .. , _ ; _ , _ , .. , _ |]" defined at level 0
with arguments constr
and "[| _ * ( _ , _ , .. , _ ) ; ( _ , _ , .. , _ ) * _ |]"
defined at level 0 with arguments constr at level 39
have incompatible prefixes. One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
[|0 * (1, 2, 3); (4, 5, 6) * false|]
: nat * nat * (nat * nat) * (nat * nat) *
(nat * bool * (nat * bool) * (nat * bool))
fun f : nat -> nat -> nat -> nat => {|f; 0; 1; 2|} : nat
: (nat -> nat -> nat -> nat) -> nat
{|fun x : nat => x + x; 0|}
: nat
{|op; 0; 1|}
: nat
File "./output/Notations.v", line 196, characters 0-26:
Warning:
New coercion path [c] : nat >-> bool is ambiguous with existing
[of_nat] : nat >-> bool. [ambiguous-paths,coercions,default]
false = 0
: Prop
fun x : option nat => match x with
| SOME x0 => x0
| NONE => 0
end
: option nat -> nat
fun x : option nat => match x with
| SOME2 x0 => x0
| NONE2 => 0
end
: option nat -> nat
fun x : option nat => match x with
| SOME3 _ x0 => x0
| NONE3 _ => 0
end
: option nat -> nat
fun x : list ?T =>
match x with
| NIL => NONE3 (list ?T)
| (_ :') t => SOME3 (list ?T) t
end
: list ?T -> option (list ?T)
where
?T :
[x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1,
x0 cannot be used)
s
: s
10
: nat
fun _ : nat => 9
: nat -> nat
fun (x : nat) (p : x = x) =>
match p in (_ = n) return (n = n) with
| ONE => ONE
end = p
: forall x : nat, x = x -> Prop
fun (x : nat) (p : x = x) =>
match p in (_ = n) return (n = n) with
| 1 => 1
end = p
: forall x : nat, x = x -> Prop
bar 0
: nat
let k := rew [P] p in v in k
: P y
let k := rew [P] p in v in k
: P y
let k := rew <- [P] p in v' in k
: P x
let k := rew [P] p in v in k
: P y
let k := rew [P] p in v in k
: P y
let k := rew <- [P] p in v' in k
: P x
let k := rew [fun y : A => P y] p in v in k
: P y
let k := rew [fun y : A => P y] p in v in k
: P y
let k := rew <- [fun y : A => P y] p in v' in k
: P x
let k := rew [fun y : A => P y] p in v in k
: P y
let k := rew [fun y : A => P y] p in v in k
: P y
let k := rew <- [fun y : A => P y] p in v' in k
: P x
let k := rew dependent [P] p in v in k
: P y p
let k := rew dependent [P] p in v in k
: P y p
let k := rew dependent <- [P'] p in v' in k
: P' x (eq_sym p)
let k := rew dependent [P] p in v in k
: P y p
let k := rew dependent [P] p in v in k
: P y p
let k := rew dependent <- [P'] p in v' in k
: P' x (eq_sym p)
let k := rew dependent [P] p in v in k
: P y p
let k := rew dependent [P] p in v in k
: P y p
let k := rew dependent <- [P'] p in v' in k
: P' x (eq_sym p)
let k := rew dependent [fun y p => id (P y p)] p in v in k
: P y p
let k := rew dependent [fun y p => id (P y p)] p in v in k
: P y p
let k := rew dependent <- [fun y0 p => id (P' y0 p)] p in v' in k
: P' x (eq_sym p)
let k := rew dependent [P] p in v in k
: P y p
let k := rew dependent [P] p in v in k
: P y p
let k := rew dependent <- [P'] p in v' in k
: P' x (eq_sym p)
let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
: P y p
let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
: P y p
let k := rew dependent <- [fun y0 p0 => id (P' y0 p0)] p in v' in k
: P' x (eq_sym p)
rew dependent [P] p in v
: P y p
rew dependent <- [P'] p in v'
: P' x (eq_sym p)
rew dependent [fun a x => id (P a x)] p in v
: id (P y p)
rew dependent <- [fun a p' => id (P' a p')] p in v'
: id (P' x (eq_sym p))
[ Seitenstruktur0.102Drucken
]
|
2026-03-28
|
