Ruslan Φ.
Ruslan Φ.
Right, I remember now that Edwin emphasized that point of view a few times.
"Not being able to write any program without" is rather vague. I am sure there are ways to interpret that for and against adding `depCongX` based on availability of `congX`....
> @Russoul @gallais @joelberkeley any feedback or ideas about `Basics.Dependent` in `base`? That works for me! I don't really have a preference.
One year has passed, I barely remember the proposal I wrote myself 😆. I agree with Guillaume, AFAIK, purely positional syntax is the way Agda does it as well, it's...
I don't know, (0 _ : a) -> b looks better to me than a 0#-> b. 4 symbols for an operator that is expected to be used much is...
> Sound like the root problem is that the named explicit arguments are ambiguous with the implicit arguments. Backward compatibility aside, any problem arising from forbidding name shadowing in the...
It has something to do with ambiguous name resolution, this typechecks: ``` foo : Int -> Int foo x = case isLT of Yes' => x*2 No' => x*4 where...
@gallais Any chance you have an insight into what's going on here? I'm quite willing to fix that now.
Thanks for the pointer!
There is, but the reason is hypothetical as for now. There is some level of concern about the LSP not being flexible enough to encode all planned (but mostly theoretical)...