git.iko.soy/Idris-dev
on 4c19d46 help sign in
Idris-dev/test/interactive009/interactive009.idr
27 lines 956 B history raw
1import Data.Vect
3%default total
5data ElemBool : Eq t => t -> Vect n t -> Bool -> Type where
6 ElemBoolNil : Eq t => ElemBool {t=t} a [] False
7 ElemBoolCons : Eq t => ElemBool {t=t} x1 xs b -> ElemBool x1 (x2 :: xs) ((x1 == x2) || b)
9data IsSet : Eq t => Vect n t -> Type where
10 IsSetNil : Eq t => IsSet {t=t} []
11 IsSetCons : Eq t => ElemBool {t=t} x xs False -> IsSet xs -> IsSet (x :: xs)
13fun_1 : Eq t => (x : t) -> (xs : Vect n t) -> (b : Bool ** ElemBool x xs b)
14fun_1 x [] = (False ** ElemBoolNil)
15fun_1 x1 (x2 :: xs) =
16 let (b ** prfRec) = fun_1 x1 xs
17 in (((x1 == x2) || b) ** (ElemBoolCons prfRec))
19fun_2 : Eq t => (xs : Vect n t) -> Maybe (IsSet xs)
20fun_2 [] = Just IsSetNil
21fun_2 (x :: xs) with (fun_1 x xs)
22 fun_2 (x :: xs) | (True ** pf) = Nothing
23 fun_2 (x :: xs) | (False ** pf) with (fun_2 xs)
24 fun_2 (x :: xs) | (False ** pf) | Nothing = Nothing
25 fun_2 (x :: xs) | (False ** pf) | (Just prfRec)
26 = Just ?rec