Apply an implication to a predicate in the implicit context. The
(a ~~ n) parameter is not actually used; it's type is used to
help select a specific fact from the context.
@ -- A safe
head function, using an implicitly-passed safety
proof. head :: Fact (IsCons xs) => ([a] ~~ xs) -> a head xs =
Prelude.head (the xs)
- - Reverse, and a lemma. reverse :: ([a] ~~ xs) -> ([a] ~~
Reverse xs) revConsLemma :: Proof (IsCons xs) -> Proof (IsCons
(Reverse xs))
- - Implement a safe last function. last :: Fact (IsCons xs)
=> ([a] ~~ xs) -> a last xs = note (revConsLemma on xs) $
head (reverse xs)