fact: Definition olast `(l : list a) : Maybe a := let fix go res xs := match xs with | nil => res | cons x xs => go (Just x) xs end in go Nothing l.
imports: Coq.Lists.List Equations(Equations) Equations.Type.EqDec Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Maybe Coq.Lists.List