stg.idr

import Data.List

mutual

  data Ty = TyInt | TyFun Ty Ty | TyData DataDesc

  data DataDesc =
    MkDataDesc
      String         -- data type name
      (List ConDesc) -- list of constructors

  data ConDesc : Type where
    MkConDesc
      :  (d: DataDesc) -- parent data type
      -> (conElem ?con d) -- ?con should refer to this very value we're defining
      -> String        -- constructor name
      -> (List Ty)     -- list of fields
      -> ConDesc
  
  ||| Proof that a constructor belongs to a datatype
  conElem : ConDesc -> DataDesc -> Type
  conElem con (MkDataDesc _ constrs) = Elem con constrs