Dependent Pattern Matching [ag-0001]

{-# OPTIONS --safe --without-K #-}
module ag-0001 where

open import MLTT.Spartan

依賴類型有一些不同於常見語言的特徵，像是下面定義的這個類型

data So : 𝟚 → 𝓤₀  ̇ where
  oh : So ₁
  ho : So ₀

在模式比對時 constructor oh 跟 ho 提供了變數 b 的訊息。

xxx : {b : 𝟚} → So b → 𝟚
xxx {b} oh = b -- 這裡 b 一定是 ₁
xxx {b} ho = b -- 這裡 b 一定是 ₀