2009-10-14から1日間の記事一覧
data Bool : Set0 where true : Bool false : Bool data BoolHold : Bool -> Set0 where boolHold : (b1 : Bool) -> BoolHold b1 not : Bool -> Bool not b2 with b2 ... | true = false ... | false = true g : (b : Bool) -> BoolHold (not b) g b with b …