Translate coe constants

[gebner]

That is, translate coe to (↑ ⬝). And coeFn to (· ·).

[digama0]

I've actually been using (·) for coe

[gebner]

They are not equivalent, since (·) propagates the expected type:

variable (n : Nat)
#check ( (·) (n + n) : Int)     -- (fun a => a) (Int.ofNat n + Int.ofNat n) : Int
#check ((↑·) (n + n) : Int)     -- (fun a => Int.ofNat a) (n + n) : Int

[digama0]

Oh yeah, if it's applied then it's a different story. In that case we probably don't want to use either one and instead should use ↑, because the goal is to get Int.ofNat (n + n), not a beta redex

[gebner]

We also need to translate the ⇑ and ↥ notations (in addition to the constants).

[gebner]

I tried to do this using mathport_rules | `(coe) => `((↑)), but this is trickier than I'd thought at first.

The issue is that the coe constant is represented in Syntax as an identifier. And there's no way to distinguish an identifier in the term category from an identifier used in other syntax (e.g. in { coe := .. }).