Dependent Pattern matching

misc

{-# OPTIONS --cubical #-}
module agda.so where
open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool

data So : Bool → Type where
  oh : So true
  ho : So false

xxx : {b : Bool} → So b → Bool
xxx {b} oh = b -- b is true here
xxx {b} ho = b -- b is false here