File MakeCaseRecordSplit.agda:
record R : Set₂ where
field f : Set₁
f : R → Set₁
f x = {!x!} -- C-c C-c (split)
This produces:
MakeCaseRecordSplit.f record { f = f } = ?
Could not parse the left-hand side
MakeCaseRecordSplit.f record { f = f }
Correct would be
f record { f = f } = ?
as shadowing the function name with an argument is allowed (maybe not good style).
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4