Gabriel Ebner

Thank! bors r+

WIP, see #191.

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...

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.).)

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

bors r+

Thanks! Please remove the "awaiting-author" label in the future when you've applied the changes from code review.

There are merge conflicts now. bors d+

I completely agree with Sebastian that Nix support should not incur any costs on the non-Nix developers. I don't want to maintain and support two build systems. (And since Nix...

> I feel it should be acceptable that maintaining the flake.nix would be the responsibility of only the nix users. Then I'm okay with this PR as long as it...