mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +03:00
7733c85fd5
The old way only worked by chance, because the argumemt order happens to be the same in all cases. I noticed due to some experiments elsewhere with different ways of elaborating case, which broke that assumption. The meaning of the list of Vars is actually the opposite of what it was taken to be... fortunately, the performance works out roughly the same. Also this way is (arguably) simpler, which is usually a good sign. |
||
|---|---|---|
| .. | ||
| List | ||
| Nat | ||
| Primitives | ||
| Buffer.idr | ||
| Either.idr | ||
| Fin.idr | ||
| IOArray.idr | ||
| IORef.idr | ||
| List.idr | ||
| Maybe.idr | ||
| Morphisms.idr | ||
| Nat.idr | ||
| So.idr | ||
| Stream.idr | ||
| Strings.idr | ||
| Vect.idr | ||