Agda Verson: 3425ed5
Mimer fills hole 0 with λ () which is ill-typed. However, it fills hole 1 with foo (λ _ → tt). It seems that if some type A doesn't have exactly 1 constructor, Mimer incorrectly fills holes of type Foo (𝟘 → A).
module Auto where
data 𝟘 : Set where
record 𝟙 : Set where
constructor tt
data Foo (A : Set) : Set where
foo : A → Foo A
foo₁ : Foo (𝟘 → 𝟘)
foo₁ = {!!}
foo₂ : Foo (𝟘 → 𝟙)
foo₂ = {!!}
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