search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.19k stars 257 forks source link

Automate coercion setup #172

Open gebner opened 2 years ago

gebner commented 2 years ago

WIP, see #191.

gebner commented 2 years ago

After #191, we have an attribute for coercions that registers a function with the norm_cast module and adds a custom delaborator. There are probably still some issues with function coercions though.

What's still missing is adding the coercion instance itself. Some high-level syntax for that would be nice.

digama0 commented 1 year ago

Suggestion: @[coe] adds a Coe instance, and @[coe CoeHead] etc makes it a more specialized kind of instance.

gebner commented 1 year ago

The other question is how to indicate function/sort coercions. (With function coercions, the other unclear question is which argument should be coerced (the resulting function might be ternary, e.g.).)

digama0 commented 1 year ago

If you give CoeFn etc to the attribute then I think it can figure that out, no? It is possible that CoeFn instances could be ambiguous though. We can make up some syntax to disambiguate.

gebner commented 1 year ago

The question is whether @[coe CoeFun] def f (a : A) (b : B a) : C → D should declare CoeFun A fun a => B a → C → D or CoeFun (B a) fun _ => C → D.

(Also just realized it's called CoeFun with a u now.)

digama0 commented 1 year ago

I would default to the second one. I'm ambivalent about how to spell the disambiguator to get the first one.