You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
defclass A do
def f(x), do: x
end
defclass B do
def g(_x, y), do: y
end
defclass C do
extend A
extend B
def h(x, _y), do: x
end
Being able to write the following instance:
definst C, for: X do
def f(x), do: x.c
def h(x, y), do: {x.c, y}
end
instead of
definst B, for: X
definst A, for: X do
def f(x), do: x.value
end
definst C, for: X do
def h(x, y), do: {x.value, y}
end
is actually a huge boost in ergonomics! Languages like Lean4 allow for it and it feels really good to be able to have the compiler resolve the typeclass dependencies and inject correct functions into correct places.
Why does it have to be done?
For the following classes:
Being able to write the following instance:
instead of
is actually a huge boost in ergonomics! Languages like Lean4 allow for it and it feels really good to be able to have the compiler resolve the typeclass dependencies and inject correct functions into correct places.
see here.
How do you think does it have to be done?
definst
definst
.What do you think needs to be figured out for it to be done?
No response
The text was updated successfully, but these errors were encountered: