Idris判定結果のベクトル長

Question

Idrisでは、述語に基づいて要素を削除したい場合、filter,dropWhile、takeWhileがあります。ただし、これらの関数はすべて、従属ペア(n : Nat ** Vect n elem)を返します。

Vectタイプとして返​​される関数はありますか？私は考えることができるものについては

：

1. 変換後の長さのベクトルを示すタイプを実装Vect

2. に依存ペアに変換Hereのように、（私はどのように分からないと思いました）上記のアイデアについては、There

、（すべての再変換1のために非常に面倒なようですsult）または2（結果ベクトルの長さを示す型をそれぞれ設計する）。

このような動作を実現する方法はありますか？

dropElem : String -> Vect n String -> Vect ?resultLen String

Answer 1

たぶん、これはあなたが探しているものでしょうか？

dropElem: (s: String) -> (v: Vect n String) -> Vect (count ((/=) s) v) String 
dropElem s = filter ((/=) s) 

あなたも、既存のfilter実装再利用することができます：

import Data.Vect 

count: (ty -> Bool) -> Vect n ty -> Nat 
count f [] = 0 
count f (x::xs) with (f x) 
    | False = count f xs 
    | True = 1 + count f xs 

%hint 
countLemma: {v: Vect n ty} -> count f v `LTE` n 
countLemma {v=[]} = LTEZero 
countLemma {v=x::xs} {f} with (f x) 
    | False = lteSuccRight countLemma 
    | True = LTESucc countLemma 

filter: (f: ty -> Bool) -> (v: Vect n ty) -> Vect (count f v) ty 
filter f [] = [] 
filter f (x::xs) with (f x) 
    | False = filter f xs 
    | True = x::filter f xs 

次にあなたが詐欺これを行う

count: (ty -> Bool) -> Vect n ty -> Nat 
count f v = fst $ filter f v 

filter: (f: ty -> Bool) -> (v: Vect n ty) -> Vect (count f v) ty 
filter f v = snd $ filter f v