Given the following fragments (taken from the tutorial by Ulf Norell and James Chapman), I understand the caller of lookup must provide a proof that the index ix of the required item is valid but I just can't find the right form to do it.
data Proven-n : Set where
record Proven-y : Set where
-- using the name 'isProven' instead of 'isTrue' of the tutorial
isProven : Bool -> Set
isProven true = Proven-y
isProven false = Proven-n
lookup : {A : Set}(xs : List A)(ix : Nat) -> isProven (n < length xs) -> A
I've managed to work out the special case below, but all my attempts for a more general application of lookup, where the vector and the lookup index are produced in another function, have failed. I'd like to understand the concept of passing around proofs. Please help.
aList : List Bool
aList = true :: false :: []
aTest: Bool
aTest = lookup aList 0 (record {})
lookup
which doesn't work out for you, including any relevant definitions (like_<_
)? It's unclear to me where exactly you are stuck. – Jannis LimpergaTest : Nat -> Bool
? That would meanaTest
yields a value ofBool
for anyNat
. I'm guessing you want something likeaTest : Nat -> Maybe Bool
, returningnothing
in case the given index is out-of-bounds. – m0davislookup
. (It also would have been appropriate to declare lookup as apostulate
.) Andlookup
andaTest
contain (obvious?) typos. My suggested (but rejected) edit to the OP is here. – m0davis