Core language

Note

This is a stub

data Term = Var Int Elims
          | Def QName Elims               -- ^ @f es@, possibly a delta/iota-redex
          | Con ConHead Args              -- ^ @c vs@
          | Lam ArgInfo (Abs Term)        -- ^ Terms are beta normal. Relevance is ignored
          | Lit Literal
          | Pi (Dom Type) (Abs Type)      -- ^ dependent or non-dependent function space
          | Sort Sort
          | Level Level
          | MetaV MetaId Elims
          | DontCare Term
            -- ^ Irrelevant stuff in relevant position, but created
            --   in an irrelevant context.