diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/output/Arguments_renaming.out | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/output/Arguments_renaming.out')
-rw-r--r-- | test-suite/output/Arguments_renaming.out | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 17c80d13..c29f5649 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -6,7 +6,7 @@ The command has indeed failed with message: Argument A renamed to T. @eq_refl : forall (B : Type) (y : B), y = y -eq_refl +@eq_refl nat : forall x : nat, x = x Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x @@ -20,6 +20,7 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x +eq_refl is not universe polymorphic Arguments are renamed to B, y When applied to no arguments: Arguments B, y are implicit and maximally inserted @@ -35,6 +36,7 @@ For myEq: Argument scopes are [type_scope _ _] For myrefl: Argument scopes are [type_scope _ _] myrefl : forall (B : Type) (x : A), B -> myEq B x x +myrefl is not universe polymorphic Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] @@ -47,19 +49,21 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] -The simpl tactic unfolds myplus - when the 2nd and 3rd arguments evaluate to a constructor +The reduction tactics unfold myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.Test1.myplus -myplus +@myplus : forall Z : Type, Z -> nat -> nat -> nat Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x @@ -70,6 +74,7 @@ For myEq: Argument scopes are [type_scope type_scope _ _] For myrefl: Argument scopes are [type_scope type_scope _ _] myrefl : forall (A B : Type) (x : A), B -> myEq A B x x +myrefl is not universe polymorphic Arguments are renamed to A, C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope type_scope _ _] @@ -84,19 +89,21 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] -The simpl tactic unfolds myplus - when the 2nd and 3rd arguments evaluate to a constructor +The reduction tactics unfold myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Top.myplus -myplus +@myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: => Error: All arguments lists must declare the same names. |