This is an error:
data Bool : Set where
true false : Bool
foo : (Bool → Bool) → Bool → Bool
foo f x with f x
This is only a warning:
data Bool : Set where
true false : Bool
foo : (Bool → Bool) → Bool → Bool
foo f x with f x
foo f x | true = false
Why?
It very often happens to me that I start writing a complicated expression to pattern match on, so I write with ..., and I want to verify that this type-checks before starting to write the further clauses, so I instinctively press C-c C-l, and syntax highlighting suddenly disappears from my whole file. In those cases, I add a clause like foo f x | _ = ? just to make Agda stop complaining and let me use the hole system to interactively build up the scrutinee after with. (I've barely tried Mikan but I just tested that this happens on Mikan main.)
This is an error:
```
data Bool : Set where
true false : Bool
foo : (Bool → Bool) → Bool → Bool
foo f x with f x
```
This is only a warning:
```
data Bool : Set where
true false : Bool
foo : (Bool → Bool) → Bool → Bool
foo f x with f x
foo f x | true = false
```
Why?
It very often happens to me that I start writing a complicated expression to pattern match on, so I write `with ...`, and I want to verify that this type-checks before starting to write the further clauses, so I instinctively press C-c C-l, and syntax highlighting suddenly disappears from my whole file. In those cases, I add a clause like `foo f x | _ = ?` just to make Agda stop complaining and let me use the hole system to interactively build up the scrutinee after `with`. (I've barely tried Mikan but I just tested that this happens on Mikan `main`.)