issue defining hpow for iterating functions

Stream: new members

[Alok Singh (S1'17)]

I want to define HPow so I can do f^n. Currently I have:

def iterate (f: a → a) (n: Nat): a → a :=
  match n with
  | 0 => id
  | n' + 1 => f ∘ iterate f n'
#eval iterate Nat.succ 2 9 -- 11
-- notation f " ^ " n => iterate (f:=f)  (n:=n)
instance: HPow (f:  a → a) (n: Nat) (out: a → a) where
  hPow := iterate (f:=f) (n:=n)
#eval iterate Nat.succ 2 4 -- 6
#eval (Nat.succ ^ 3) 4 --

It errors with:

application type mismatch
  HPow f
argument
  f
has type
  a → a : Sort ?u.3591
but is expected to have type
  Type ?u.3589 : Type (?u.3589 + 1)

I'm not sure where the metavars are coming in from.

[Eric Wieser]

Are you aware of docs#Nat.iterate ?

[Alok Singh (S1'17)]

now i am, thanks. reading the source to see how to impl my own version.

[Eric Wieser]

You might also be interested in docs#Function.End

[Kyle Miller]

The errors are that HPow takes three types, and you're giving it three terms.

[Kyle Miller]

This typechecks:

instance {a : Type*} : HPow (a → a) Nat (a → a) where
  hPow := Nat.iterate

And this works

#check (Nat.succ ^ 3)

However, it appears this fails to typecheck:

#check (Nat.succ ^ 3) 1

[Kyle Miller]

It seems to be that the elaborator can't see that this is a function.

[Alok Singh (S1'17)]

what does the star after type mean?

[Kyle Miller]

You can use this trick though:

#eval (Nat.succ ^ 3 :) 1

[Kyle Miller]

Type* is a mathlib notation, and it's like Type _ but it ensures the universe level is a fresh level variable.

[Kyle Miller]

You can use Type _ here.