mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-16 07:34:45 +03:00
32e26c5bd1
Instead of having UN & RF (& Hole in the near future & maybe even more later e.g. operator names) we have a single UN constructor that takes a UserName instead of a String. UserName is (for now) ```idris data UserName : Type where Basic : String -> UserName -- default name constructor e.g. map Field : String -> UserName -- field accessor e.g. .fst Underscore : UserName -- no name e.g. _ ``` This is extracted from the draft PR #1852 which is too big to easily debug. Once this is working, I can go back to it. |
||
---|---|---|
.. | ||
DerivingEq.idr | ||
expected | ||
run | ||
test.idr |