This code does not work since polarity of Nat (monotone in i) is only inferred when the constructors are given. But it is already needed for checking sub.
data Nat : {i : Size} -> Set
sub : {i : Size} -> Nat {i} → Nat {↑ i}
sub x = x
data Nat where
zero : {i : Size} -> Nat {↑ i}
suc : {i : Size} -> Nat {i} -> Nat {↑ i}
Original issue reported on code.google.com by andreas....@gmail.com on 19 Feb 2012 at 10:21
Attachments:
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