doesnt-compute.idr

module LLC

consume : Nat -> List (Maybe Nat) -> List (Maybe Nat)
consume vid (Nothing :: vs) = Nothing :: consume vid vs
consume vid (Just v :: vs) with (vid == v)
  | True = Nothing :: vs
  | False = Just v :: consume vid vs

data Lolli : Type -> Type -> Type where
  mkLolli : (a -> b) -> Lolli a b
  
data Lin : Nat -> List (Maybe Nat) -> List (Maybe Nat) -> Type -> Type where
  llam : (((v : Nat) -> (i : List (Maybe Nat)) -> Lin v       i                (consume vid i) a) ->
                                                  Lin (S vid) (Just vid :: hi) (Nothing :: ho) b
         ) -> 
         Lin vid hi ho (Lolli a b)
  lapp : Lin vid hi h (Lolli a b) -> Lin vid h ho a -> Lin vid hi ho b