With standard library:
import Level open Level using (Level; 0ℓ) 1ℓ : Level 1ℓ = Level.zero 0ℓ
Error is:
error: [ShouldBePi]
Level should be a function type, but it isn't
when checking that 0ℓ is a valid argument to a function of type Level
One would expect a complaint that Level.zero is not a function type...
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