■

data Nat : Set0
  where
    zero : Nat
    succ : Nat -> Nat

data NatHold : Nat -> Set0
  where
    natHold : (n : Nat) -> NatHold n

test : (x : Nat) -> NatHold x
test x with x
test x | zero with x
test x | zero | zero = natHold zero
test x | zero | succ a = natHold zero
test x | succ a with x
test x | succ a | zero = natHold (succ a)
test x | succ a | succ b = natHold (succ a)

これはなんかなー。

xがzero ∧ succ aみたいな事はそもそもありえない系だと思うのでぷるぷる

ななし

data Nat : Set0
  where
    zero : Nat
    succ : Nat -> Nat

data NatHold : Nat -> Set0
  where
    natHold : (n : Nat) -> NatHold n

g : Nat -> Nat
g x = zero

f : (x' : Nat) -> NatHold (g x')
f x with g x
... | zero = natHold zero
... | succ a = natHold (succ a)

こういう複合的に酷そうなものも存在する。これはpatternのカバレッジを全部書けっていうのも重なっている。

多分一度中を見てcase式の全組合せを掻き集めてそれら全てで型チェックするって感じなんだろうかなぁ・・・。