module LinearScan.NonEmpty where


import Debug.Trace (trace, traceShow, traceShowId)
import qualified Prelude
import qualified Data.IntMap
import qualified Data.IntSet
import qualified Data.List
import qualified Data.Ord
import qualified Data.Functor.Identity
import qualified Hask.Utils


coq_NonEmpty_rect :: (a1 -> a2) -> (a1 -> ([] a1) -> a2 -> a2) -> ([] 
                     a1) -> a2
coq_NonEmpty_rect f f0 n =
  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
    (\y ->
    f y)
    (\y n0 ->
    f0 y n0 (coq_NonEmpty_rect f f0 n0))
    n

coq_NonEmpty_rec :: (a1 -> a2) -> (a1 -> ([] a1) -> a2 -> a2) -> ([] 
                    a1) -> a2
coq_NonEmpty_rec =
  coq_NonEmpty_rect

coq_NE_from_list :: a1 -> ([] a1) -> [] a1
coq_NE_from_list x xs =
  case xs of {
   [] -> (:[]) x;
   (:) y ys -> (:) x (coq_NE_from_list y ys)}