Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
module Main
import Data.Vect
import Data.Fin
%default total
find : Eq x => List x -> x -> Maybe Int
find [] elem = Nothing
find (y :: xs) elem = if y == elem then (Just 0) else (map (\ n => n + 1) (find xs elem))
find2 : Eq x => {n : Nat} -> Vect n x -> x -> Maybe (Fin n)
find2 [] elem = Nothing
find2 (y :: xs) elem = if y == elem then (Just FZ) else (map FS (find2 xs elem))
ex : find2 [1, 2, 3] 2 = Just 1
ex = Refl
nothingProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> Not (Elem e v) -> (find2 v e) = Nothing
nothingProof n v elem notIn = ?noIdea1
justProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> (find2 v e = Just r) -> (index r v == e) = True
justProof n v elem findProof = ?noIdea2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.