coercion to function notation

Stream: lean4

[Kevin Buzzard]

I can't get ⇑f notation. What am I doing wrong?

structure AutomorphicForm where
  toFun      : Nat → Int
  cool_axiom : toFun 37 = 42

variable (f : AutomorphicForm) (n : Nat)

namespace AutomorphicForm

-- #check f n  -- error
#check f.toFun n -- f.toFun n : Int
-- #check ⇑f n -- error

instance : CoeFun AutomorphicForm (fun _ => Nat → Int) :=
  ⟨toFun⟩

#check f n -- f.toFun n : Int
#check f.toFun n -- f.toFun n : Int
#check ⇑f n -- f.toFun n : Int

attribute [coe] toFun

#check f n -- ↑f n : Int
#check f.toFun n -- ↑f n : Int
#check ⇑f n -- ↑f n : Int

-- How do I get `⇑f` ?

[llllvvuu]

#check ⇑f works for me

instance : CoeFun AutomorphicForm (fun _ => Nat → Int) :=
  ⟨toFun⟩

#check f n -- f.toFun n : Int
#check f.toFun n -- f.toFun n : Int
#check ⇑f n -- f.toFun n : Int
#check ⇑f -- f.toFun : Nat → Int

attribute [coe] toFun

#check f n -- ↑f n : Int
#check f.toFun n -- ↑f n : Int
#check ⇑f n -- ↑f n : Int
#check ⇑f -- ↑f : Nat → Int

[Floris van Doorn]

I think ⇑ is just always printed as ↑?

[Eric Wieser]

import Lean.Elab.Command

structure AutomorphicForm where
  toFun      : Nat → Int
  cool_axiom : toFun 37 = 42

variable (f : AutomorphicForm) (n : Nat)

namespace AutomorphicForm

-- #check f n  -- error
#check f.toFun n -- f.toFun n : Int
-- #check ⇑f n -- error

instance : CoeFun AutomorphicForm (fun _ => Nat → Int) :=
  ⟨toFun⟩

#check f n -- f.toFun n : Int
#check f.toFun n -- f.toFun n : Int
#check ⇑f n -- f.toFun n : Int

-- this is what `@[coe]` does, but we use `.coeFun`
run_cmd Lean.Elab.Command.liftTermElabM do
  Lean.Meta.registerCoercion ``AutomorphicForm.toFun
    (some { numArgs := 1, coercee := 0, type := .coeFun })

#check ⇑f -- ⇑f : Nat → Int
#check f n -- f n : Int
#check f.toFun n -- f n : Int
#check ⇑f n -- f n : Int

[Eric Wieser]

We never bothered adding @[coe_fun] to match @[coe], because mathlib only uses it for DFunLike.coe anyway.