error.idris

module Main

import Data.Nat

-- Linearity

infixr 0 #->, ?->

(#->) : Type -> Type -> Type
a #-> b = (1 _ : a) -> b

(?->) : Type -> Type -> Type
a ?-> b = (0 _ : a) -> b


data Stack_ : Nat -> Type -> Type where
  CONS : Stack_ i a -> Stack_ i a

data Debits_ : (d : Type) -> Nat -> Stack_ i a -> Type where
  DTwo   :                Debits_ d (acc + i) s #-> Debits_ d acc (CONS s)
  DThree :                Debits_ d  acc      s #-> Debits_ d acc (CONS s)

ddecr : Debits_ d (S acc) s #-> Debits_ d acc s

dpush_ : {i : Nat} -> {0 s : Stack_ i a} -> (0 one : 1 `LTE` i) ->
  Debits_ d 1 s #-> Debits_ d i s
dpush_ one (DTwo ds) =
  let ds' = ddecr ds in
  DThree ds'