filter : {X : Set0} -> (X -> Bool) -> List X -> List X filter p [] = [] filter p (x :: xs) with p x ... | true = filter p xs -- x :: (filter p xs) ... | false = filter p xsfilterをこう書き直して、つまり、[]しか返さないんですけれども、これ…

でません・・・。 natEq : Nat -> Nat -> Bool natEq zero zero = true natEq zero (succ b) = false natEq (succ a) zero = false natEq (succ a) (succ b) = natEq a b boolEq : Bool -> Bool -> Bool boolEq true true = true boolEq false false = true …

natRight : {a : Nat} {b : Nat} -> a NatPair b -> Nat natRight (a natPair b) = b getNatRight : {a : Nat} {b : Nat} -> a NatPair b -> Val b getNatRight (a natPair b) = val b valNat : (a : Nat) -> Val a valNat a = val a body : (length (filter…

けれども、分かりません・・・。 module QSort where open import Data.List open import Data.Bool open import Data.Product data Nat : Set0 where zero : Nat succ : Nat -> Nat Length : {A : Set0} -> List A -> Nat Length [] = zero Length (x &#875…