Consider the following Agda file:
variable a : Set data C (a : Set) : Set where member : C a → a → a member _ w = w
Running agda with -v tc.proj.like:50 reports the following:
checkDecl: checking projection-likeness of [RollbackWindow.C]
RollbackWindow.C is abstract or not a function, thus, not considered for projection-likeness
checkDecl: checking projection-likeness of [RollbackWindow.member, RollbackWindow..generalizedField-a,
RollbackWindow.GeneralizeTel, RollbackWindow.mkGeneralizeTel]
mutual definitions are not considered for projection-likeness
and indeed the function is not considered to be projection-like. However, if one makes the {a : Set} -> explicit in the type of member then it is considered so:
checkDecl: checking projection-likeness of [RollbackWindow.C]
RollbackWindow.C is abstract or not a function, thus, not considered for projection-likeness
checkDecl: checking projection-likeness of [RollbackWindow.member]
Checking for projection likeness
member : {a : Set} → C a → a → a
candidates: [(RollbackWindow.C, 1)]
member : {a : Set} → C a → a → a
is projection like in argument 1 for type C
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