module Language.Reflection.TT public exportFilePos : TypeFilePos = (Int, Int) public exportdata FC : Type where     MkFC : String -> FilePos -> FilePos -> FC     EmptyFC : FC public exportemptyFC : FCemptyFC = EmptyFC public exportdata NameType : Type where     Bound   : NameType     Func    : NameType     DataCon : (tag : Int) -> (arity : Nat) -> NameType     TyCon   : (tag : Int) -> (arity : Nat) -> NameType public exportdata Constant    = I Int    | BI Integer    | Str String    | Ch Char    | Db Double    | WorldVal     | IntType    | IntegerType    | StringType    | CharType    | DoubleType    | WorldType public exportdata Name = UN String          | MN String Int          | NS (List String) Name public exportdata Count = M0 | M1 | MW public exportdata PiInfo = ImplicitArg | ExplicitArg | AutoImplicit public exportdata IsVar : Name -> Nat -> List Name -> Type where     First : IsVar n Z (n :: ns)     Later : IsVar n i ns -> IsVar n (S i) (m :: ns) public exportdata LazyReason = LInf | LLazy | LUnknown -- Type checked terms in the core TTpublic exportdata TT : List Name -> Type where     Local : FC -> (idx : Nat) -> (n : Name) ->             (0 prf : IsVar name idx vars) -> TT vars     Ref : FC -> NameType -> Name -> TT vars     Pi : FC -> Count -> PiInfo ->          (x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) ->          TT vars     Lam : FC -> Count -> PiInfo ->           (x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) ->           TT vars     App : FC -> TT vars -> TT vars -> TT vars     TDelayed : FC -> LazyReason -> TT vars -> TT vars     TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars     TForce : FC -> TT vars -> TT vars     PrimVal : FC -> Constant -> TT vars     Erased : FC -> TT vars     TType : FC -> TT vars public exportdata Visibility = Private | Export | Public