Impressum Notations4.out
Sprache: unbekannt
|
|
Haftungsausschluß.out KontaktUnknown {[0] [0] [0]}diese Dinge liegen außhalb unserer Verantwortung
[< 0 > + < 1 > * < 2 >]
: nat
Entry custom:myconstr is
[ "6" RIGHTA
[ ]
| "5" RIGHTA
[ SELF; "+"; NEXT ]
| "4" RIGHTA
[ SELF; "*"; NEXT ]
| "3" RIGHTA
[ "<"; term LEVEL "10"; ">" ] ]
[< b > + < b > * < 2 >]
: nat
[<< # 0 >>]
: option nat
[b + c]
: nat
fun a : nat => [a + a]
: nat -> nat
File "./output/Notations4.v", line 38, characters 0-88:
Warning: This notation will not be used for printing as it is bound to a
single variable. [notation-bound-to-variable,parsing,default]
[1 {f 1}]
: Expr
fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
: nat -> Expr -> Expr -> Expr
fun e : Expr =>
match e with
| [x y + z] => [x + y z]
| [1 + 1] => [1]
| _ => [e + e]
end
: Expr -> Expr
[(1 + 1)]
: Expr
myAnd1 True True
: Prop
r 2 3
: Prop
let v := 0%test17 in v : myint63
: myint63
fun y : nat => # (x, z) |-> y & y
: forall y : nat,
(?T * ?T0 -> ?T * ?T0 * nat) * (?T1 * ?T2 -> ?T1 * ?T2 * nat)
where
?T :
[y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0 |- Type] (pat,
p0, p cannot be used)
?T0 :
[y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0 |- Type] (pat,
p0, p cannot be used)
?T1 :
[y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2
|- Type] (pat, p0, p cannot be used)
?T2 :
[y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2
|- Type] (pat, p0, p cannot be used)
fun y : nat => # (x, z) |-> (x + y) & (y + z)
: forall y : nat,
(nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat)
where
?T :
[y : nat pat : nat * ?T p0 : nat * ?T p := p0 : nat * ?T |- Type] (pat,
p0, p cannot be used)
?T0 :
[y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat
|- Type] (pat, p0, p cannot be used)
fun '{| |} => true
: R -> bool
File "./output/Notations4.v", line 149, characters 82-85:
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
File "./output/Notations4.v", line 153, characters 76-78:
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
File "./output/Notations4.v", line 157, characters 78-81:
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
File "./output/Notations4.v", line 161, characters 52-55:
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
Entry custom:expr is
[ "201" RIGHTA
[ "{"; term LEVEL "200"; "}" ] ]
fun x : nat => [ x ]
: nat -> nat
fun x : nat => [x]
: nat -> nat
∀ x : nat, x = x
: Prop
File "./output/Notations4.v", line 195, characters 0-160:
Warning: Notation "∀ _ .. _ , _" was already defined with a different format
in scope type_scope. [notation-incompatible-format,parsing,default]
∀x : nat,x = x
: Prop
File "./output/Notations4.v", line 208, characters 0-60:
Warning: Notation "_ %%% _" was already defined with a different format.
[notation-incompatible-format,parsing,default]
File "./output/Notations4.v", line 212, characters 0-64:
Warning: Notation "_ %%% _" was already defined with a different format.
[notation-incompatible-format,parsing,default]
File "./output/Notations4.v", line 217, characters 0-62:
Warning: Lonely notation "_ %%%% _" was already defined with a different
format. [notation-incompatible-format,parsing,default]
3 %% 4
: nat
3 %% 4
: nat
3 %% 4
: nat
File "./output/Notations4.v", line 245, characters 47-59:
Warning: The format modifier is irrelevant for only-parsing rules.
[irrelevant-format-only-parsing,parsing,default]
File "./output/Notations4.v", line 249, characters 36-48:
Warning: The only parsing modifier has no effect in Reserved Notation.
[irrelevant-reserved-notation-only-parsing,parsing,default]
fun x : nat => U (S x)
: nat -> nat
V tt
: unit * (unit -> unit)
fun x : nat => V x
: forall x : nat, nat * (?T -> ?T)
where
?T : [x : nat |- Type]
File "./output/Notations4.v", line 266, characters 0-30:
Warning: Notation "_ :=: _" was already used.
[notation-overridden,parsing,default]
0 :=: 0
: Prop
fun x : nat => <{ x; (S x) }>
: nat -> nat
Set
: Type
fun x : nat => S x
: nat -> nat
True
: Prop
exists p : nat, ▢_p (p >= 1)
: Prop
▢_n (n >= 1)
: Prop
File "./output/Notations4.v", line 336, characters 17-20:
The command has indeed failed with message:
Found an inductive type while a variable name was expected.
File "./output/Notations4.v", line 337, characters 17-18:
The command has indeed failed with message:
Found a constructor while a variable name was expected.
File "./output/Notations4.v", line 339, characters 17-18:
The command has indeed failed with message:
Found a constant while a variable name was expected.
exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2)
: Prop
▢_n (n >= 1)
: Prop
File "./output/Notations4.v", line 352, characters 17-20:
The command has indeed failed with message:
Found an inductive type while a pattern was expected.
▢_tt (tt = tt)
: Prop
File "./output/Notations4.v", line 355, characters 17-18:
The command has indeed failed with message:
Found a constant while a pattern was expected.
exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2)
: Prop
pseudo_force n (fun n : nat => n >= 1)
: Prop
File "./output/Notations4.v", line 368, characters 17-20:
The command has indeed failed with message:
Found an inductive type while a pattern was expected.
▢_tt (tt = tt)
: Prop
File "./output/Notations4.v", line 371, characters 17-18:
The command has indeed failed with message:
Found a constant while a pattern was expected.
exists x y : nat, myforce (x, y) (x >= 1 /\ y >= 2)
: Prop
myforce n (n >= 1)
: Prop
File "./output/Notations4.v", line 383, characters 21-24:
The command has indeed failed with message:
Found an inductive type while a pattern was expected.
myforce tt (tt = tt)
: Prop
File "./output/Notations4.v", line 386, characters 21-22:
The command has indeed failed with message:
Found a constant while a pattern was expected.
id nat
: Set
fun a : bool => id a
: bool -> bool
fun nat : bool => id nat
: bool -> bool
File "./output/Notations4.v", line 398, characters 17-20:
The command has indeed failed with message:
Found an inductive type while a pattern was expected.
!! nat, nat = true
: Prop
!!! nat, nat = true
: Prop
!!!! (nat, id), nat = true /\ id = false
: Prop
∀ x : nat, x = 0
: Prop
∀₁ x, x = 0
: Prop
∀₁ x, x = 0
: Prop
∀₂ x y, x + y = 0
: Prop
((1, 2))
: nat * nat
%% [x == 1]
: Prop
%%% [1]
: Prop
[[2]]
: nat * nat
%%%
: Type
## (x, _) (x = 0)
: Prop
File "./output/Notations4.v", line 494, characters 21-30:
The command has indeed failed with message:
Unexpected type constraint in notation already providing a type constraint.
## '(x, y) (x + y = 0)
: Prop
## x (x = 0)
: Prop
## '(x, y) (x = 0)
: Prop
fun f : ## a (a = 0) => f 1 eq_refl
: ## a (a = 0) -> 1 = 0
[MyNotation 0]
: nat
fun MyNone : nat => MyNone
: nat -> nat
MyNone+
: option ?A
where
?A : [ |- Type]
Some MyNone+
: option (option ?A)
where
?A : [ |- Type]
0+
: option ?A
where
?A : [ |- Type]
0+
: option ?A
where
?A : [ |- Type]
0
: nat
File "./output/Notations4.v", line 544, characters 0-78:
The command has indeed failed with message:
Notation "func _ .. _ , _" is already defined at level 200 with arguments
binder, constr at next level while it is now required to be at level 200
with arguments constr, constr at next level.
File "./output/Notations4.v", line 549, characters 0-57:
The command has indeed failed with message:
Notation "[[ _ ]]" is already defined at level 0 with arguments custom foo
while it is now required to be at level 0 with arguments custom bar.
lambda x y : nat, x + y = 0
: nat -> nat -> Prop
((!!nat) + bool)%type
: Set
fun z : nat => (z, 1, z, 2)
: nat -> nat * nat * nat * nat
fun z : nat => [(!!z) + z]
: nat -> nat * nat * nat * nat * nat
uncurryλ a b c => a + b + c
: unit * nat * nat * nat -> nat
fun x : unit * nat * (nat * nat) =>
match x with
| (x0, y) =>
match y with
| (a, b) =>
let d := 1 in
match x0 with
| (x1, c) => let 'tt := x1 in a + b + c + d
end
end
end
: unit * nat * (nat * nat) -> nat
fun x : unit * nat * (nat * nat) =>
match x with
| (x0, (a, b)) => let d := 1 in match x0 with
| (tt, c) => a + b + c + d
end
end
: unit * nat * (nat * nat) -> nat
uncurryλ '(a, b) => a + b
: unit * (nat * nat) -> nat
lets a b c := 0 in a + b + c
: nat
let
'(a, b) := (0, 0) in
lets d := 1 in let '(c, e) := (0, 0) in a + b + c + d + e
: nat
[ Seitenstruktur0.83Drucken
]
|
2026-03-28
|
