Indexing terms with versioning.

repl.txt

λΠ> :t Deprecated.L (N 2) (L (N 1) (B False))
L (N 2) (L (N 1) (B False)) : Term ?ctxt (Just 1) TyNat
λΠ> :t L (S "w") (L (N 1) (B False))
L (S "w") (L (N 1) (B False)) : Term ?ctxt Nothing TyNat
λΠ> 

Versioned.idr

module Versioned

import Data.List.Elem
import Data.List.Quantifiers
import Data.Nat

%default total

data Ty
  = TyNat
  | TyBool
  | TyString

namespace Simple
  public export
  data Term : List (Nat, Ty) -> Nat -> Ty -> Type
    where
      N : Nat -> Term ctxt 0 TyNat
      B : Bool -> Term ctxt 1 TyNat
      V : Elem (v,type) ctxt -> Term ctxt v type

      L : Term              ctxt  v         a
       -> Term (MkPair v a::ctxt) w         b
       -> Term              ctxt  (max v w) b

namespace Deprecated

  public export
  cmp : (a,b : Maybe Nat) -> Maybe Nat
  cmp a b = max <$> a <*> b

  public export
  data Term : List (Maybe Nat, Ty) -> Maybe Nat -> Ty -> Type
    where
      D : Term ctxt v type
        -> Term ctxt Nothing type
      S : String -> Term ctxt (Just 1) TyString
      N : Nat -> Term ctxt (Just 0) TyNat
      B : Bool -> Term ctxt (Just 1) TyNat
      V : Elem (v,type) ctxt -> Term ctxt v type

      L : Term              ctxt  v         a
       -> Term (MkPair v a::ctxt) w         b
       -> Term              ctxt  (cmp v w) b