diff options
Diffstat (limited to 'test-suite/output/Arguments.out')
| -rw-r--r-- | test-suite/output/Arguments.out | 88 |
1 files changed, 52 insertions, 36 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 7c9b1e27..629a1ab6 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,94 +1,110 @@ -minus : nat -> nat -> nat +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +The reduction tactics unfold Nat.sub but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus when applied to 1 argument - avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +The reduction tactics unfold Nat.sub when applied to 1 argument + but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus +The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and - when applied to 1 argument avoiding to expose match constructs -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat + when applied to 1 argument but avoid exposing match constructs +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus - when the 1st and 2nd arguments evaluate to a constructor and - when applied to 2 arguments -minus is transparent -Expands to: Constant Coq.Init.Peano.minus -minus : nat -> nat -> nat +The reduction tactics unfold Nat.sub when the 1st and + 2nd arguments evaluate to a constructor and when applied to 2 arguments +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub +Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] -The simpl tactic unfolds minus - when the 1st and 2nd arguments evaluate to a constructor -minus is transparent -Expands to: Constant Coq.Init.Peano.minus +The reduction tactics unfold Nat.sub when the 1st and + 2nd arguments evaluate to a constructor +Nat.sub is transparent +Expands to: Constant Coq.Init.Nat.sub pf : forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 +pf is not universe polymorphic Arguments D2, C2 are implicit Arguments D1, C1 are implicit and maximally inserted Argument scopes are [foo_scope type_scope _ _ _ _ _] -The simpl tactic never unfolds pf +The reduction tactics never unfold pf pf is transparent Expands to: Constant Top.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C +fcomp is not universe polymorphic Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] -The simpl tactic unfolds fcomp when applied to 6 arguments +The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Top.fcomp volatile : nat -> nat +volatile is not universe polymorphic Argument scope is [nat_scope] -The simpl tactic always unfolds volatile +The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Top.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] f is transparent Expands to: Constant Top.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 3rd, 4th and 5th arguments evaluate to a constructor +The reduction tactics unfold f when the 3rd, 4th and + 5th arguments evaluate to a constructor f is transparent Expands to: Constant Top.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 4th, 5th and 6th arguments evaluate to a constructor +The reduction tactics unfold f when the 4th, 5th and + 6th arguments evaluate to a constructor f is transparent Expands to: Constant Top.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] -The simpl tactic unfolds f - when the 5th, 6th and 7th arguments evaluate to a constructor +The reduction tactics unfold f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f + = forall v : unit, f 0 0 5 v 3 = 2 + : Prop + = 2 = 2 + : Prop f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat -The simpl tactic unfolds f - when the 5th, 6th and 7th arguments evaluate to a constructor +f is not universe polymorphic +The reduction tactics unfold f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Top.f forall w : r, w 3 true = tt |