atが書けないぴーーーーーーー
data Unit : Set0 where unit : Unit data Nat : Set0 where zero : Nat succ : Nat -> Nat data Bool : Set0 where true : Bool false : Bool _+_ : Nat -> Nat -> Nat zero + b = b (succ a) + b = succ (a + b) data Hold (T : Set0) : Set0 where hold : Nat -> T -> Hold T Vec : Nat -> Set0 Vec zero = Unit Vec (succ a) = Hold (Vec a) vappend : (m n : Nat) -> Vec m -> Vec n -> Vec (m + n) vappend zero b as bs = bs vappend (succ a) b (hold elem as') bs = hold elem (vappend a b as' bs) at : (m n : Nat) -> Vec n -> Nat -- m < n ???
at : (m n : Nat) -> Vec n -> Id Bool (m < n) true -> Nat的な事をしてただまぁこの形だとdot-patternとか出て来ちゃいそうなソレなので色々遠回りすると出来そうですね。
というか多分dot-patternとImplicit Parameterを使わないというなぞの縛りを設けるならば、Leibniz Equalityの方が良い筈。