mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-01 06:12:57 +03:00
6c7f13d128
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.
13 lines
738 B
Plaintext
13 lines
738 B
Plaintext
Processing as TTImp
|
|
Written TTC
|
|
Yaffle> Bye for now!
|
|
Processing as TTImp
|
|
Dot2.yaff:15:10--15:15:Can't match on ($resolved73 ?{P:n:92}_[] ?{P:m:92}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:n:92}_[] ?{P:n:92}_[])
|
|
Yaffle> Bye for now!
|
|
Processing as TTImp
|
|
Dot3.yaff:18:10--18:15:Can't match on ($resolved73 ?{P:x:100}_[] ?{P:y:100}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?Main.{_:30}_[] ?Main.{_:29}_[])
|
|
Yaffle> Bye for now!
|
|
Processing as TTImp
|
|
Dot4.yaff:17:10--17:15:Can't match on ($resolved73 ?Main.{_:32}_[] ?Main.{_:31}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:x:100}_[] ?{P:y:100}_[])
|
|
Yaffle> Bye for now!
|