diff options
Diffstat (limited to 'test-suite/output')
31 files changed, 278 insertions, 155 deletions
diff --git a/test-suite/output/Arith.out b/test-suite/output/Arith.out deleted file mode 100644 index 210dd6ad..00000000 --- a/test-suite/output/Arith.out +++ /dev/null @@ -1,4 +0,0 @@ -[n:nat](S (S n)) - : nat->nat -[n:nat](S (plus n n)) - : nat->nat diff --git a/test-suite/output/Arith.v b/test-suite/output/Arith.v deleted file mode 100644 index 39989dfc..00000000 --- a/test-suite/output/Arith.v +++ /dev/null @@ -1,2 +0,0 @@ -Check [n](S (S n)). -Check [n](S (plus n n)). diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 5f13caaf..63137edb 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -1,4 +1,9 @@ t_rect = -[P:(t->Type); f:([x:=t](x0:x)(P x0)->(P (k x0)))] - Fix F{F [t:t] : (P t) := <P>Cases t of (k x x0) => (f x0 (F x0)) end} - : (P:(t->Type))([x:=t](x0:x)(P x0)->(P (k x0)))->(t:t)(P t) +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 x 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 + diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 7483e8c4..452d3603 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -1,5 +1,6 @@ (* Cases with let-in in constructors types *) -Inductive t : Set := k : [x:=t]x -> x. +Inductive t : Set := + k : let x := t in x -> x. Print t_rect. diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out index 63e042d8..4b8aa355 100644 --- a/test-suite/output/Coercions.out +++ b/test-suite/output/Coercions.out @@ -1,4 +1,6 @@ -(P x) +P x : Prop -(R x x) +R x x : Prop +fun (x : foo) (n : nat) => x n + : foo -> nat -> nat diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index 61b69038..c88b143f 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -1,9 +1,15 @@ (* Submitted by Randy Pollack *) -Record pred [S:Set]: Type := { sp_pred :> S -> Prop }. -Record rel [S:Set]: Type := { sr_rel :> S -> S -> Prop }. +Record pred (S : Set) : Type := {sp_pred :> S -> Prop}. +Record rel (S : Set) : Type := {sr_rel :> S -> S -> Prop}. Section testSection. -Variables S: Set; P: (pred S); R: (rel S); x:S. +Variables (S : Set) (P : pred S) (R : rel S) (x : S). Check (P x). Check (R x x). +End testSection. + +(* Check the removal of coercions with target Funclass *) + +Record foo : Type := {D :> nat -> nat}. +Check (fun (x : foo) (n : nat) => x n). diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out new file mode 100644 index 00000000..62c9d395 --- /dev/null +++ b/test-suite/output/Fixpoint.out @@ -0,0 +1,11 @@ +fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : +list B := match l with + | nil => nil (A:=B) + | a :: l0 => f a :: F A B f l0 + end + : forall A B : Set, (A -> B) -> list A -> list B +let fix f (m : nat) : nat := match m with + | 0 => 0 + | S m' => f m' + end in f 0 + : nat diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 270fff4e..fc27e8d2 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -1,7 +1,18 @@ -Require PolyList. +Require Import List. + +Check + (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : + list B := match l with + | nil => nil + | a :: l => f a :: F _ _ f l + end). + +(* V8 printing of this term used to failed in V8.0 and V8.0pl1 (cf bug #860) *) +Check + let fix f (m : nat) : nat := + match m with + | O => 0 + | S m' => f m' + end + in f 0. -Check Fix F { F/4 : (A,B:Set)(A->B)->(list A)->(list B) := - [_,_,f,l]Cases l of - nil => (nil ?) - | (cons a l) => (cons (f a) (F ? ? f l)) - end}. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index f9cf9efc..38c5b827 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -1,5 +1,10 @@ -d2 = [x:nat](d1 1!x) - : (x,x0:nat)x0=x ->x0=x +compose (C:=nat) S + : (nat -> nat) -> nat -> nat +ex_intro (P:=fun _ : nat => True) (x:=0) I + : ex (fun _ : nat => True) +d2 = fun x : nat => d1 (y:=x) + : forall x x0 : nat, x0 = x -> x0 = x -Positions [1; 2] are implicit + +Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 2dea0d18..0ff7e87f 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -1,18 +1,19 @@ Set Implicit Arguments. +Unset Strict Implicit. (* Suggested by Pierre Casteran (bug #169) *) (* Argument 3 is needed to typecheck and should be printed *) -Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)). -Check (compose 3!nat S). +Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x). +Check (compose (C:=nat) S). (* Better to explicitly display the arguments inferable from a position that could disappear after reduction *) -Inductive ex [A:Set;P:A->Prop] : Prop - := ex_intro : (x:A)(P x)->(ex P). -Check (ex_intro 2![_]True 3!O I). +Inductive ex (A : Set) (P : A -> Prop) : Prop := + ex_intro : forall x : A, P x -> ex P. +Check (ex_intro (P:=fun _ => True) (x:=0) I). (* Test for V8 printing of implicit by names *) -Definition d1 [y;x;h:x=y:>nat] := h. -Definition d2 [x] := (!d1 x). +Definition d1 y x (h : x = y :>nat) := h. +Definition d2 x := d1 (y:=x). Print d2. diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index d7120f89..4ed72c50 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,6 +1,10 @@ -Inductive sig2 [A : Set; P : A->Prop; Q : A->Prop] : Set := - exist2 : (x:A)(P x)->(Q x)->(sig2 A P Q) -(EX x:nat|x=x) +Inductive sig2 (A : Set) (P : A -> Prop) (Q : A -> Prop) : Set := + exist2 : forall x : A, P x -> Q x -> sig2 P Q +For sig2: Argument A is implicit +For exist2: Argument A is implicit +For sig2: Argument scopes are [type_scope type_scope type_scope] +For exist2: Argument scopes are [type_scope _ _ _ _ _] +exists x : nat, x = x : Prop -[b:bool](if b then b else b) - : bool->bool +fun b : bool => if b then b else b + : bool -> bool diff --git a/test-suite/output/InitSyntax.v b/test-suite/output/InitSyntax.v index 90fad371..eb39782e 100644 --- a/test-suite/output/InitSyntax.v +++ b/test-suite/output/InitSyntax.v @@ -1,4 +1,4 @@ (* Soumis par Pierre *) -Print sig2. -Check (EX x:nat|x=x). -Check [b:bool]if b then b else b. +Print sig2. +Check (exists x : nat, x = x). +Check (fun b : bool => if b then b else b). diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out index cadb35c6..5831c9f4 100644 --- a/test-suite/output/Intuition.out +++ b/test-suite/output/Intuition.out @@ -2,6 +2,6 @@ m : Z n : Z - H : `m >= n` + H : (m >= n)%Z ============================ - `m >= m` + (m >= m)%Z diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v index c0508c90..5f1914d2 100644 --- a/test-suite/output/Intuition.v +++ b/test-suite/output/Intuition.v @@ -1,5 +1,5 @@ -Require ZArith_base. -Goal (m,n:Z) `m >= n` -> `m >= m` /\ `m >= n`. -Intros; Intuition. +Require Import ZArith_base. +Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z. +intros; intuition. Show. Abort. diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out index 505821d7..d0f15f0e 100644 --- a/test-suite/output/Nametab.out +++ b/test-suite/output/Nametab.out @@ -1,27 +1,35 @@ -id is not a defined object -K.id is not a defined object -N.K.id is not a defined object Constant Top.Q.N.K.id + (shorter name to refer to it in current context is Q.N.K.id) Constant Top.Q.N.K.id -K is not a defined object -N.K is not a defined object + (shorter name to refer to it in current context is Q.N.K.id) +Constant Top.Q.N.K.id + (shorter name to refer to it in current context is Q.N.K.id) +Constant Top.Q.N.K.id +Constant Top.Q.N.K.id + (shorter name to refer to it in current context is Q.N.K.id) +No module is referred to by basename K +No module is referred to by name N.K Module Top.Q.N.K Module Top.Q.N.K -N is not a defined object +No module is referred to by basename N Module Top.Q.N Module Top.Q.N Module Top.Q Module Top.Q -id is not a defined object Constant Top.Q.N.K.id -N.K.id is not a defined object + (shorter name to refer to it in current context is K.id) +Constant Top.Q.N.K.id +Constant Top.Q.N.K.id + (shorter name to refer to it in current context is K.id) Constant Top.Q.N.K.id + (shorter name to refer to it in current context is K.id) Constant Top.Q.N.K.id + (shorter name to refer to it in current context is K.id) Module Top.Q.N.K -N.K is not a defined object +No module is referred to by name N.K Module Top.Q.N.K Module Top.Q.N.K -N is not a defined object +No module is referred to by basename N Module Top.Q.N Module Top.Q.N Module Top.Q diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v index 61966c7c..a1a7579b 100644 --- a/test-suite/output/Nametab.v +++ b/test-suite/output/Nametab.v @@ -1,7 +1,7 @@ Module Q. Module N. Module K. - Definition id:=Set. + Definition id := Set. End K. End N. End Q. @@ -12,18 +12,17 @@ End Q. (* OK *) Locate Q.N.K.id. (* OK *) Locate Top.Q.N.K.id. -(* Bad *) Locate K. -(* Bad *) Locate N.K. -(* OK *) Locate Q.N.K. -(* OK *) Locate Top.Q.N.K. +(* Bad *) Locate Module K. +(* Bad *) Locate Module N.K. +(* OK *) Locate Module Q.N.K. +(* OK *) Locate Module Top.Q.N.K. -(* Bad *) Locate N. -(* OK *) Locate Q.N. -(* OK *) Locate Top.Q.N. - -(* OK *) Locate Q. -(* OK *) Locate Top.Q. +(* Bad *) Locate Module N. +(* OK *) Locate Module Q.N. +(* OK *) Locate Module Top.Q.N. +(* OK *) Locate Module Q. +(* OK *) Locate Module Top.Q. Import Q.N. @@ -35,14 +34,14 @@ Import Q.N. (* OK *) Locate Q.N.K.id. (* OK *) Locate Top.Q.N.K.id. -(* OK *) Locate K. -(* Bad *) Locate N.K. -(* OK *) Locate Q.N.K. -(* OK *) Locate Top.Q.N.K. +(* OK *) Locate Module K. +(* Bad *) Locate Module N.K. +(* OK *) Locate Module Q.N.K. +(* OK *) Locate Module Top.Q.N.K. -(* Bad *) Locate N. -(* OK *) Locate Q.N. -(* OK *) Locate Top.Q.N. +(* Bad *) Locate Module N. +(* OK *) Locate Module Q.N. +(* OK *) Locate Module Top.Q.N. -(* OK *) Locate Q. -(* OK *) Locate Top.Q. +(* OK *) Locate Module Q. +(* OK *) Locate Module Top.Q. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out new file mode 100644 index 00000000..3ab3de45 --- /dev/null +++ b/test-suite/output/Notations.out @@ -0,0 +1,24 @@ +true ? 0; 1 + : nat +if true as x return (x ? nat; bool) then 0 else true + : true ? nat; bool +Defining 'proj1' as keyword +fun e : nat * nat => proj1 e + : nat * nat -> nat +Defining 'decomp' as keyword +decomp (true, true) as t, u in (t, u) + : bool * bool +!(0 = 0) + : Prop +forall n : nat, n = 0 + : Prop +!(0 = 0) + : Prop +3 + 3 + : Z +3 + 3 + : znat +[1; 2; 4] + : list nat +(1; 2, 4) + : nat * nat * nat diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v new file mode 100644 index 00000000..4382975e --- /dev/null +++ b/test-suite/output/Notations.v @@ -0,0 +1,68 @@ +(**********************************************************************) +(* Notations for if and let (submitted by Roland Zumkeller) *) + +Notation "a ? b ; c" := (if a then b else c) (at level 10). + +Check (true ? 0 ; 1). +Check if true as x return (if x then nat else bool) then 0 else true. + +Notation "'proj1' t" := (let (a,_) := t in a) (at level 1). + +Check (fun e : nat * nat => proj1 e). + +Notation "'decomp' a 'as' x , y 'in' b" := (let (x,y) := a in b) (at level 1). + +Check (decomp (true,true) as t, u in (t,u)). + +(**********************************************************************) +(* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *) + +Notation "! A" := (forall _:nat, A) (at level 60). + +Check ! (0=0). +Check forall n, n=0. +Check forall n:nat, 0=0. + +(**********************************************************************) +(* Conflict between notation and notation below coercions *) + +(* Case of a printer conflict *) + +Require Import BinInt. +Coercion Zpos : positive >-> Z. +Open Scope Z_scope. + + (* Check that (Zpos 3) is better printed by the printer for Z than + by the printer for positive *) + +Check (3 + Zpos 3). + +(* Case of a num printer only below coercion (submitted by Georges Gonthier) *) + +Open Scope nat_scope. + +Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). +Coercion Zpos: nat >-> znat. + +Delimit Scope znat_scope with znat. +Open Scope znat_scope. + +Variable addz : znat -> znat -> znat. +Notation "z1 + z2" := (addz z1 z2) : znat_scope. + + (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit, + is printed the same way, and not "S 2 + S 2" as if numeral printing was + only tested with coercion still present *) + +Check (3+3). + +(**********************************************************************) +(* Check recursive notations *) + +Require Import List. +Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). +Check [1;2;4]. + +Reserved Notation "( x ; y , .. , z )" (at level 0). +Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z). +Check (1;2,4). diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index fa30656b..e6f7556d 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -1,4 +1,4 @@ -``32`` +32%R : R -``-31`` +(-31)%R : R diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index d976dcc1..15ae6601 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -1,3 +1,3 @@ -Require Reals. -Check ``32``. -Check ``-31``. +Require Import Reals. +Check 32%R. +Check (-31)%R. diff --git a/test-suite/output/Remark2.out b/test-suite/output/Remark2.out deleted file mode 100644 index adabc2fe..00000000 --- a/test-suite/output/Remark2.out +++ /dev/null @@ -1 +0,0 @@ -B.C.t is not a defined object diff --git a/test-suite/output/Remark2.v b/test-suite/output/Remark2.v deleted file mode 100644 index e1ef57a0..00000000 --- a/test-suite/output/Remark2.v +++ /dev/null @@ -1,8 +0,0 @@ -Section A. -Section B. -Section C. -Remark t : True. Proof I. -End C. -End B. -End A. -Locate B.C.t. diff --git a/test-suite/output/Sum.out b/test-suite/output/Sum.out index 22422602..bda6a68b 100644 --- a/test-suite/output/Sum.out +++ b/test-suite/output/Sum.out @@ -1,6 +1,6 @@ -nat+nat+{True} +nat + nat + {True} : Set -{True}+{True}+{True} +{True} + {True} + {True} : Set -nat+{True}+{True} +nat + {True} + {True} : Set diff --git a/test-suite/output/Sum.v b/test-suite/output/Sum.v index aceadd12..f12285a6 100644 --- a/test-suite/output/Sum.v +++ b/test-suite/output/Sum.v @@ -1,3 +1,3 @@ -Check nat+nat+{True}. -Check {True}+{True}+{True}. -Check nat+{True}+{True}. +Check (nat + nat + {True}). +Check ({True} + {True} + {True}). +Check (nat + {True} + {True}). diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out new file mode 100644 index 00000000..71c59e43 --- /dev/null +++ b/test-suite/output/Tactics.out @@ -0,0 +1 @@ +intro H; split; [ a H | e H ]. diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v new file mode 100644 index 00000000..24a33651 --- /dev/null +++ b/test-suite/output/Tactics.v @@ -0,0 +1,9 @@ +(* Test printing of Tactic Notation *) + +Tactic Notation "a" constr(x) := apply x. +Tactic Notation "e" constr(x) := exact x. + +Lemma test : True -> True /\ True. +intro H; split; [a H|e H]. +Show Script. +Qed. diff --git a/test-suite/output/TranspModtype.v b/test-suite/output/TranspModtype.v index 27b1fb9f..68eff33a 100644 --- a/test-suite/output/TranspModtype.v +++ b/test-suite/output/TranspModtype.v @@ -1,17 +1,17 @@ Module Type SIG. - Axiom A:Set. - Axiom B:Set. + Axiom A : Set. + Axiom B : Set. End SIG. -Module M:SIG. - Definition A:=nat. - Definition B:=nat. +Module M : SIG. + Definition A := nat. + Definition B := nat. End M. -Module N<:SIG:=M. +Module N <: SIG := M. -Module TranspId[X:SIG] <: SIG with Definition A:=X.A := X. -Module OpaqueId[X:SIG] : SIG with Definition A:=X.A := X. +Module TranspId (X: SIG) <: SIG with Definition A := X.A := X. +Module OpaqueId (X: SIG) : SIG with Definition A := X.A := X. Module TrM := TranspId M. Module OpM := OpaqueId M. diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out index 0fdc5b7e..cbfb9f20 100644 --- a/test-suite/output/ZSyntax.out +++ b/test-suite/output/ZSyntax.out @@ -1,26 +1,26 @@ -`32` +32%Z : Z -[f:(nat->Z)]`(f O)+0` - : (nat->Z)->Z -[x:positive](POS (xO x)) - : positive->Z -[x:positive]`(POS x)+1` - : positive->Z -[x:positive](POS x) - : positive->Z -[x:positive](NEG (xO x)) - : positive->Z -[x:positive]`(POS (xO x))+0` - : positive->Z -[x:positive]`(Zopp (POS (xO x)))` - : positive->Z -[x:positive]`(Zopp (POS (xO x)))+0` - : positive->Z -`(inject_nat (0))+1` +fun f : nat -> Z => (f 0%nat + 0)%Z + : (nat -> Z) -> Z +fun x : positive => Zpos (xO x) + : positive -> Z +fun x : positive => (Zpos x + 1)%Z + : positive -> Z +fun x : positive => Zpos x + : positive -> Z +fun x : positive => Zneg (xO x) + : positive -> Z +fun x : positive => (Zpos (xO x) + 0)%Z + : positive -> Z +fun x : positive => (- Zpos (xO x))%Z + : positive -> Z +fun x : positive => (- Zpos (xO x) + 0)%Z + : positive -> Z +(Z_of_nat 0 + 1)%Z : Z -`0+(inject_nat (plus (0) (0)))` +(0 + Z_of_nat (0 + 0))%Z : Z -`(inject_nat (0)) = 0` +Z_of_nat 0 = 0%Z : Prop -`0+(inject_nat (11))` +(0 + Z_of_nat 11)%Z : Z diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index 49442b75..289a1e3f 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -1,17 +1,17 @@ -Require ZArith. -Check `32`. -Check [f:nat->Z]`(f O) + 0`. -Check [x:positive]`(POS (xO x))`. -Check [x:positive]`(POS x)+1`. -Check [x:positive]`(POS x)`. -Check [x:positive]`(NEG (xO x))`. -Check [x:positive]`(POS (xO x))+0`. -Check [x:positive]`(Zopp (POS (xO x)))`. -Check [x:positive]`(Zopp (POS (xO x)))+0`. -Check `(inject_nat O)+1`. -Check (Zplus `0` (inject_nat (plus O O))). -Check `(inject_nat O)=0`. +Require Import ZArith. +Check 32%Z. +Check (fun f : nat -> Z => (f 0%nat + 0)%Z). +Check (fun x : positive => Zpos (xO x)). +Check (fun x : positive => (Zpos x + 1)%Z). +Check (fun x : positive => Zpos x). +Check (fun x : positive => Zneg (xO x)). +Check (fun x : positive => (Zpos (xO x) + 0)%Z). +Check (fun x : positive => (- Zpos (xO x))%Z). +Check (fun x : positive => (- Zpos (xO x) + 0)%Z). +Check (Z_of_nat 0 + 1)%Z. +Check (0 + Z_of_nat (0 + 0))%Z. +Check (Z_of_nat 0 = 0%Z). (* Submitted by Pierre Casteran *) -Require Arith. -Check (Zplus `0` (inject_nat (11))). +Require Import Arith. +Check (0 + Z_of_nat 11)%Z. diff --git a/test-suite/output/implicits.out b/test-suite/output/implicits.out deleted file mode 100644 index e4837199..00000000 --- a/test-suite/output/implicits.out +++ /dev/null @@ -1,4 +0,0 @@ -(compose 3!nat S) - : (nat->nat)->nat->nat -(ex_intro 2![_:nat]True 3!(0) I) - : (ex [_:nat]True) diff --git a/test-suite/output/implicits.v b/test-suite/output/implicits.v deleted file mode 100644 index d7ea7227..00000000 --- a/test-suite/output/implicits.v +++ /dev/null @@ -1,13 +0,0 @@ -Set Implicit Arguments. - -(* Suggested by Pierre Casteran (bug #169) *) -(* Argument 3 is needed to typecheck and should be printed *) -Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)). -Check (compose 3!nat S). - -(* Better to explicitly display the arguments inferable from a - position that could disappear after reduction *) -Inductive ex [A:Set;P:A->Prop] : Prop - := ex_intro : (x:A)(P x)->(ex P). -Check (ex_intro 2![_]True 3!O I). - |