PartialFunction

Partial Function Pattern

module partial_template where

{- TODO: describe the difference between data and
  record without using terms like eta-equality and
  beta-reduction -}
data FalseSet : Set where
record TrueSet : Set where

data Bool : Set where
  False : Bool
  True : Bool

boolid : Bool -> Bool
boolid a = a

_IsTrue : Bool -> Set
True IsTrue = TrueSet
False IsTrue = FalseSet

{- The hidden argument is only defined where the argument
   is true. Since the alternative part of the domain
   (where the argument is false) doesn't provide any value
   for the "IsTrue" test, the function as a whole is still
   total -}
only_applied_to_true : (a : Bool) -> {_ : (boolid a) IsTrue} -> Bool
only_applied_to_true True = True
only_applied_to_true False {} {- This clause is absurd but it needn't be
  this clause is protected by the hidden argument and can't ever happen -}

good = only_applied_to_true True
fail = only_applied_to_true False