Quelle  wish_18097.out   Sprache: unbekannt

Notation pow := Nat.pow

Nat.pow =
fix pow (n m : nat) {struct m} : nat :=
  match m with
  | 0 => 1
  | S m0 => n * pow n m0
  end
     : nat -> nat -> nat

Arguments Nat.pow (n m)%_nat_scope
Notation pow := Nat.pow
Expands to: Notation wish_18097.pow
Declared in library wish_18097, line 1, characters 0-24

Nat.pow : nat -> nat -> nat

Nat.pow is not universe polymorphic
Arguments Nat.pow (n m)%_nat_scope
Nat.pow is transparent
Expands to: Constant Corelib.Init.Nat.pow
Declared in library Corelib.Init.Nat, line 143, characters 9-12