diff options
Diffstat (limited to 'test-suite/output/PrintInfos.out')
| -rw-r--r-- | test-suite/output/PrintInfos.out | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index e0fb7d5a9..62889f802 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,5 +1,6 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} +existT is template universe polymorphic Argument A is implicit Argument scopes are [type_scope _ _ _] Expands to: Constructor Coq.Init.Specif.existT @@ -24,6 +25,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 monomorphic When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: @@ -44,9 +46,11 @@ fix plus (n m : nat) {struct n} : nat := end : nat -> nat -> nat +plus is monomorphic Argument scopes are [nat_scope nat_scope] plus : nat -> nat -> nat +plus is monomorphic Argument scopes are [nat_scope nat_scope] plus is transparent Expands to: Constant Coq.Init.Peano.plus @@ -54,6 +58,7 @@ plus : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 +plus_n_O is monomorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O @@ -75,11 +80,13 @@ For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set +comparison is monomorphic Expands to: Inductive Coq.Init.Datatypes.comparison Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo +bar is monomorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -87,12 +94,14 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] +bar is monomorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted bar : foo +bar is monomorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -100,6 +109,7 @@ Argument x is implicit and maximally inserted Expands to: Constant Top.bar *** [ bar : foo ] +bar is monomorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 |