edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-02 22:43:14 +03:00
Code Issues Projects Releases Wiki Activity
6dd9c1296f
Idris2-boot/tests/ttimp/dot001/expected

16 lines
927 B
Plaintext
Raw Normal View History

Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone.
2019-05-25 20:39:21 +03:00
Processing as TTImp
Written TTC
Yaffle> Bye for now!
Processing as TTImp
Check names are visible/public
2019-06-24 02:12:58 +03:00
Dot2.yaff:15:1--16:1:When elaborating left hand side of Main.half:
Chapter 11 examples now working
2019-07-09 00:46:20 +03:00
Dot2.yaff:15:10--15:15:Can't match on ($resolved86 ?{P:n:94}_[] ?{P:m:94}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved86 ?{P:n:94}_[] ?{P:n:94}_[])
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone.
2019-05-25 20:39:21 +03:00
Yaffle> Bye for now!
Processing as TTImp
Check names are visible/public
2019-06-24 02:12:58 +03:00
Dot3.yaff:18:1--20:1:When elaborating left hand side of Main.addBaz3:
Chapter 11 examples now working
2019-07-09 00:46:20 +03:00
Dot3.yaff:18:10--18:15:Can't match on ($resolved86 ?{P:x:99}_[] ?{P:x:99}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved86 ?{P:x:99}_[] ?{P:x:99}_[])
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone.
2019-05-25 20:39:21 +03:00
Yaffle> Bye for now!
Processing as TTImp
Improve dot patterns Allow matching rather than unification, as long as it doesn't solve any metavariables on the way. I noticed a potential unification bug on the way, forgetting to update whether holes are solved when unifying argument lists.
2019-07-05 01:16:08 +03:00
Dot4.yaff:13:1--16:1:When elaborating left hand side of Main.addBaz:
Chapter 11 examples now working
2019-07-09 00:46:20 +03:00
Dot4.yaff:13:9--13:14:Can't match on ($resolved86 ?{P:x:93}_[] ?{P:y:93}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved86 ?{P:x:93}_[] ?{P:y:93}_[])
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone.
2019-05-25 20:39:21 +03:00
Yaffle> Bye for now!
Reference in New Issue Copy Permalink