From 9e44bd9d77025c06d39a69b953e001721a0ce650 Mon Sep 17 00:00:00 2001 From: Asher Frost Date: Sun, 31 Aug 2025 15:34:34 -0400 Subject: [PATCH 1/2] docs: added library documentation for `Elab` --- libs/base/Language/Reflection.idr | 42 +++---- libs/base/Language/Reflection/TT.idr | 49 +++++--- libs/base/Language/Reflection/TTImp.idr | 145 ++++++++++++++++-------- 3 files changed, 152 insertions(+), 84 deletions(-) diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr index 4667249e056..4ba29b1a61a 100644 --- a/libs/base/Language/Reflection.idr +++ b/libs/base/Language/Reflection.idr @@ -62,49 +62,49 @@ data Elab : Type -> Type where ResugarTerm : (maxLineWidth : Maybe Nat) -> TTImp -> Elab String - -- Elaborate a TTImp term to a concrete value + ||| Elaborate a TTImp term to a concrete value Check : TTImp -> Elab expected - -- Quote a concrete expression back to a TTImp + ||| Quote a concrete expression back to a TTImp Quote : (0 _ : val) -> Elab TTImp - -- Elaborate under a lambda + ||| Elaborate under a lambda Lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val)) - -- Get the current goal type, if known - -- (it might need to be inferred from the solution) + ||| Get the current goal type, if known + ||| (it might need to be inferred from the solution) Goal : Elab (Maybe TTImp) - -- Get the names of local variables in scope + ||| Get the names of local variables in scope LocalVars : Elab (List Name) - -- Generate a new unique name, based on the given string + ||| Generate a new unique name, based on the given string GenSym : String -> Elab Name - -- Put a name in the current namespace + ||| Put a name in the current namespace InCurrentNS : Name -> Elab Name - -- Get the types of every name which matches. - -- There may be ambiguities - returns a list of fully explicit names - -- and their types. If there's no results, the name is undefined. + ||| Get the types of every name which matches. + ||| There may be ambiguities - returns a list of fully explicit names + ||| and their types. If there's no results, the name is undefined. GetType : Name -> Elab (List (Name, TTImp)) - -- Get the metadata associated with a name + ||| Get the metadata associated with a name GetInfo : Name -> Elab (List (Name, NameInfo)) - -- Get the visibility associated with a name + ||| Get the visibility associated with a name GetVis : Name -> Elab (List (Name, Visibility)) - -- Get the type of a local variable + ||| Get the type of a local variable GetLocalType : Name -> Elab TTImp - -- Get the constructors of a data type. The name must be fully resolved. + ||| Get the constructors of a data type. The name must be fully resolved. GetCons : Name -> Elab (List Name) - -- Get all function definition names referred in a definition. The name must be fully resolved. + ||| Get all function definition names referred in a definition. The name must be fully resolved. GetReferredFns : Name -> Elab (List Name) - -- Get the name of the current and outer functions, if it is applicable + ||| Get the name of the current and outer functions, if it is applicable GetCurrentFn : Elab (SnocList Name) - -- Check a group of top level declarations + ||| Check a group of top level declarations Declare : List Decl -> Elab () - -- Read the contents of a file, if it is present + ||| Read the contents of a file, if it is present ReadFile : LookupDir -> (path : String) -> Elab $ Maybe String - -- Writes to a file, replacing existing contents, if were present + ||| Writes to a file, replacing existing contents, if were present WriteFile : LookupDir -> (path : String) -> (contents : String) -> Elab () - -- Returns the specified type of dir related to the current idris project + ||| Returns the specified type of dir related to the current idris project IdrisDir : LookupDir -> Elab String export diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr index e19aa0e1513..ea58965316c 100644 --- a/libs/base/Language/Reflection/TT.idr +++ b/libs/base/Language/Reflection/TT.idr @@ -6,14 +6,14 @@ import public Data.String import Decidable.Equality %default total - +||| namespace, stored in reverse order public export -data Namespace = MkNS (List String) -- namespace, stored in reverse order +data Namespace = MkNS (List String) %name Namespace ns - +||| module identifier, stored in reverse order public export -data ModuleIdent = MkMI (List String) -- module identifier, stored in reverse order +data ModuleIdent = MkMI (List String) %name ModuleIdent mi @@ -27,9 +27,9 @@ export Show Namespace where show (MkNS ns) = showSep "." (reverse ns) --- 'FilePos' represents the position of --- the source information in the file (or REPL). --- in the form of '(line-no, column-no)'. +||| 'FilePos' represents the position of +||| the source information in the file (or REPL). +||| in the form of '(line-no, column-no)'. public export FilePos : Type FilePos = (Int, Int) @@ -187,6 +187,7 @@ Show Constant where show (PrT x) = show x show WorldVal = "%World" +||| Any name that a user can assign to public export data UserName = Basic String -- default name constructor e.g. map @@ -195,14 +196,23 @@ data UserName %name UserName un -public export -data Name = NS Namespace Name -- name in a namespace - | UN UserName -- user defined name - | MN String Int -- machine generated name - | DN String Name -- a name and how to display it - | Nested (Int, Int) Name -- nested function name - | CaseBlock String Int -- case block nested in (resolved) name - | WithBlock String Int -- with block nested in (resolved) name +||| A name in a Idris program +public export +data Name = + ||| A qualified name + NS Namespace Name + ||| A user defined name + | UN UserName + ||| A machine generated name + | MN String Int + ||| A name with a display string + | DN String Name + ||| Nested function name + | Nested (Int, Int) Name + ||| Case block nested in (resolved) name + | CaseBlock String Int + ||| With block nested in (resolved) name + | WithBlock String Int %name Name nm @@ -251,8 +261,15 @@ record NameInfo where constructor MkNameInfo nametype : NameType +||| A multiplicity public export -data Count = M0 | M1 | MW +data Count = + ||| 0 (erased) + M0 | + ||| 1 (linear) + M1 | + ||| ω (unrestricted) + MW %name Count rig export diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 8bab4ab8bcc..3013c6b7a86 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -29,66 +29,96 @@ mutual | UnderAppliedCon %name DotReason dr + ||| The elaborator representation of an Idris term + ||| All of these take a file context `FC` as their first argument public export data TTImp : Type where + ||| A variable reference, by name IVar : FC -> Name -> TTImp - IPi : FC -> Count -> PiInfo TTImp -> Maybe Name -> + ||| A function type, of the form `(mult binder : argTy) -> retTy`, with implicitness determined by `info` + IPi : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) -> (argTy : TTImp) -> (retTy : TTImp) -> TTImp - ILam : FC -> Count -> PiInfo TTImp -> Maybe Name -> + ||| A lambda abstraction, of the form`\(mult binder : argTy) => retTy`, with implicitness determined by `info` + ILam : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) -> (argTy : TTImp) -> (lamTy : TTImp) -> TTImp - ILet : FC -> (lhsFC : FC) -> Count -> Name -> + ||| A let binding, of the form `let mult var : nTy = nVal in scope` + ILet : FC -> (lhsFC : FC) -> (mult : Count) -> (var : Name) -> (nTy : TTImp) -> (nVal : TTImp) -> (scope : TTImp) -> TTImp - ICase : FC -> List FnOpt -> TTImp -> (ty : TTImp) -> - List Clause -> TTImp - ILocal : FC -> List Decl -> TTImp -> TTImp - IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp - - IApp : FC -> TTImp -> TTImp -> TTImp - INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp - IAutoApp : FC -> TTImp -> TTImp -> TTImp + ||| A case expression `case val : ty of clauses` + ICase : FC -> (opts : List FnOpt) -> (val : TTImp) -> (ty : TTImp) -> + (clauses : List Clause) -> TTImp + ||| A list of full declarations local to a term + ILocal : FC -> (context : List Decl) -> (term : TTImp) -> TTImp + ||| An update to a record value, `{ updates } val` + IUpdate : FC -> (updates : List IFieldUpdate) -> (val : TTImp) -> TTImp + + ||| A function application, `f x` + IApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp + ||| A named function application (for named parameters), e.g, `f {arg=x}` + INamedApp : FC -> (f : TTImp) -> (arg : Name) -> (x : TTImp) -> TTImp + ||| An explicitly inserted auto implicit, `f @{x}` + IAutoApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp + ||| A view in a `with` rule IWithApp : FC -> TTImp -> TTImp -> TTImp + ||| `%search` ISearch : FC -> (depth : Nat) -> TTImp + ||| This operation is for expression that tries to typecheck expression in the list according to the given AltType and return either one of them, or default one (if present in the AltType), or fails IAlternative : FC -> AltType -> List TTImp -> TTImp - IRewrite : FC -> TTImp -> TTImp -> TTImp + ||| A rewrite expression, `rewrite eq in exp` + IRewrite : FC -> (eq : TTImp) -> (exp : TTImp) -> TTImp - -- Any implicit bindings in the scope should be bound here, using - -- the given binder + ||| Any implicit bindings in the scope should be bound here, using + ||| the given binder IBindHere : FC -> BindMode -> TTImp -> TTImp - -- A name which should be implicitly bound + ||| A name which should be implicitly bound IBindVar : FC -> Name -> TTImp - -- An 'as' pattern, valid on the LHS of a clause only - IAs : FC -> (nameFC : FC) -> UseSide -> Name -> TTImp -> TTImp - -- A 'dot' pattern, i.e. one which must also have the given value - -- by unification + ||| An 'as' pattern, valid on the LHS of a clause only, `group@pat` + IAs : FC -> (nameFC : FC) -> UseSide -> (group : Name) -> (pat : TTImp) -> TTImp + ||| A 'dot' pattern, i.e. one which must also have the given value + ||| by unification, `.(...)` IMustUnify : FC -> DotReason -> TTImp -> TTImp -- Laziness annotations - IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type - IDelay : FC -> TTImp -> TTImp -- delay constructor + ||| The delay type, `Delay t` + IDelayed : FC -> LazyReason -> TTImp -> TTImp + ||| The constructor of `Delay`, `delay t` + IDelay : FC -> TTImp -> TTImp + ||| `force` IForce : FC -> TTImp -> TTImp - -- Quasiquotation + ||| Quasi-quotation of expression (`( ... )) IQuote : FC -> TTImp -> TTImp + ||| Quasi-quotation of a name (`{ ... }) IQuoteName : FC -> Name -> TTImp + ||| Quasi-quotation of a list of declarations (`[ ... ]) IQuoteDecl : FC -> List Decl -> TTImp + ||| Unquote of an expression (~e) IUnquote : FC -> TTImp -> TTImp - + ||| A primitive value, such as an integer or string constant. + ||| Also any primitive *type*, apart from `Type` itself IPrimVal : FC -> (c : Constant) -> TTImp + ||| The type `Type` IType : FC -> TTImp + ||| A named hole IHole : FC -> String -> TTImp - -- An implicit value, solved by unification, but which will also be - -- bound (either as a pattern variable or a type variable) if unsolved - -- at the end of elaborator + ||| An implicit value, solved by unification, but which will also be + ||| bound (either as a pattern variable or a type variable) if unsolved + ||| at the end of elaborator. + ||| Note that `Implicit False` is `?`, while `Implicit True` is `_` Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp - IWithUnambigNames : FC -> List (FC, Name) -> TTImp -> TTImp + ||| `with name exp` + IWithUnambigNames : FC -> (name : List (FC, Name)) -> (exp : TTImp) -> TTImp %name TTImp s, t, u + ||| A record field update public export data IFieldUpdate : Type where + ||| `path := val` ISetField : (path : List String) -> TTImp -> IFieldUpdate + ||| `path $= val` ISetFieldApp : (path : List String) -> TTImp -> IFieldUpdate %name IFieldUpdate upd @@ -105,22 +135,23 @@ mutual NoInline : FnOpt Deprecate : FnOpt TCInline : FnOpt - -- Flag means the hint is a direct hint, not a function which might - -- find the result (e.g. chasing parent interface dictionaries) + ||| Flag means the hint is a direct hint, not a function which might + ||| find the result (e.g. chasing parent interface dictionaries) Hint : Bool -> FnOpt - -- Flag means to use as a default if all else fails + ||| `%globalhint` if true, `%defaulthint` if false GlobalHint : Bool -> FnOpt ExternFn : FnOpt - -- Defined externally, list calling conventions + ||| Defined externally, list calling conventions ForeignFn : List TTImp -> FnOpt - -- Mark for export to a foreign language, list calling conventions + ||| Mark for export to a foreign language, list calling conventions ForeignExport : List TTImp -> FnOpt - -- assume safe to cancel arguments in unification + ||| assume safe to cancel arguments in unification Invertible : FnOpt Totality : TotalReq -> FnOpt + ||| `%macro` Macro : FnOpt SpecArgs : List Name -> FnOpt - + ||| A name with an associated type public export data ITy : Type where MkTy : FC -> (n : WithFC Name) -> (ty : TTImp) -> ITy @@ -129,11 +160,16 @@ mutual public export data DataOpt : Type where - SearchBy : List1 Name -> DataOpt -- determining arguments - NoHints : DataOpt -- Don't generate search hints for constructors - UniqueSearch : DataOpt -- auto implicit search must check result is unique - External : DataOpt -- implemented externally - NoNewtype : DataOpt -- don't apply newtype optimisation + ||| Determining arguments + SearchBy : List1 Name -> DataOpt + ||| Don't generate search hints for constructors + NoHints : DataOpt + ||| Auto implicit search must check result is unique + UniqueSearch : DataOpt + ||| Implemented externally + External : DataOpt + ||| Don't apply newtype optimization + NoNewtype : DataOpt %name DataOpt dopt @@ -165,15 +201,18 @@ mutual public export data WithFlag = Syntactic - + ||| A clause in a function definition public export data Clause : Type where + ||| A simple pattern PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause + ||| A pattern with views WithClause : FC -> (lhs : TTImp) -> (rig : Count) -> (wval : TTImp) -> -- with'd expression (& quantity) (prf : Maybe (Count, Name)) -> -- optional name for the proof (& quantity) (flags : List WithFlag) -> List Clause -> Clause + ||| An impossible pattern ImpossibleClause : FC -> (lhs : TTImp) -> Clause %name Clause cl @@ -209,22 +248,34 @@ mutual (opts : List FnOpt) -> (type : ITy) -> IClaimData - + ||| A top-level declaration public export data Decl : Type where - IClaim : WithFC IClaimData -> Decl - IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl - IDef : FC -> Name -> (cls : List Clause) -> Decl + ||| A type ascription, `a : b`. + ||| Called a claim because of Curry Howard, the statement `x : p` is equivalent to `x` is a proof of `p`. + IClaim : (claim : WithFC IClaimData) -> Decl + ||| A data declaration + IData : FC -> (vis : WithDefault Visibility Private) -> Maybe TotalReq -> (cons : Data) -> Decl + ||| A function definition by its clauses + IDef : FC -> (f : Name) -> (cls : List Clause) -> Decl + ||| A parameter block IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) -> (decls : List Decl) -> Decl + ||| A record declaration + ||| @ ns Nested namespace IRecord : FC -> - Maybe String -> -- nested namespace - WithDefault Visibility Private -> - Maybe TotalReq -> Record -> Decl + (ns : Maybe String) -> + (vis : WithDefault Visibility Private) -> + (totality : Maybe TotalReq) -> (rec : Record) -> Decl + ||| A namespace declaration, `namespace ns where decls` INamespace : FC -> Namespace -> (decls : List Decl) -> Decl + ||| A transformation declaration ITransform : FC -> Name -> TTImp -> TTImp -> Decl + ||| A top-level elaboration run IRunElabDecl : FC -> TTImp -> Decl + ||| A logging directive ILog : Maybe (List String, Nat) -> Decl + ||| A builtin declaration, `%builtin type name` IBuiltin : FC -> BuiltinType -> Name -> Decl %name Decl decl From 17616e9b9ba4116b426eb46e0d297255a495fb05 Mon Sep 17 00:00:00 2001 From: Asher Frost Date: Mon, 1 Sep 2025 09:55:12 -0400 Subject: [PATCH 2/2] fix: made doc changes non-breaking --- libs/base/Language/Reflection/TT.idr | 40 +++++++++--------- libs/base/Language/Reflection/TTImp.idr | 56 ++++++++++++------------- 2 files changed, 48 insertions(+), 48 deletions(-) diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr index ea58965316c..77bd70fb57b 100644 --- a/libs/base/Language/Reflection/TT.idr +++ b/libs/base/Language/Reflection/TT.idr @@ -8,7 +8,7 @@ import Decidable.Equality %default total ||| namespace, stored in reverse order public export -data Namespace = MkNS (List String) +data Namespace = MkNS (List String) %name Namespace ns ||| module identifier, stored in reverse order @@ -198,21 +198,21 @@ data UserName ||| A name in a Idris program public export -data Name = - ||| A qualified name - NS Namespace Name - ||| A user defined name - | UN UserName - ||| A machine generated name - | MN String Int - ||| A name with a display string - | DN String Name - ||| Nested function name - | Nested (Int, Int) Name - ||| Case block nested in (resolved) name - | CaseBlock String Int - ||| With block nested in (resolved) name - | WithBlock String Int +data Name : Type where + ||| A qualified name + NS : Namespace -> Name -> Name + ||| A user defined name + UN : UserName -> Name + ||| A machine generated name + MN : String -> Int -> Name + ||| A name with a display string + DN : String -> Name -> Name + ||| Nested function name + Nested : (Int, Int) -> Name -> Name + ||| Case block nested in (resolved) name + CaseBlock : String -> Int -> Name + ||| With block nested in (resolved) name + WithBlock : String -> Int -> Name %name Name nm @@ -263,13 +263,13 @@ record NameInfo where ||| A multiplicity public export -data Count = +data Count : Type where ||| 0 (erased) - M0 | + M0 : Count ||| 1 (linear) - M1 | + M1 : Count ||| ω (unrestricted) - MW + MW : Count %name Count rig export diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 3013c6b7a86..154d046ea6c 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -33,40 +33,40 @@ mutual ||| All of these take a file context `FC` as their first argument public export data TTImp : Type where - ||| A variable reference, by name + ||| A variable reference, by name IVar : FC -> Name -> TTImp - ||| A function type, of the form `(mult binder : argTy) -> retTy`, with implicitness determined by `info` + ||| A function type, of the form `(mult binder : argTy) -> retTy`, with implicitness determined by `info` IPi : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) -> (argTy : TTImp) -> (retTy : TTImp) -> TTImp - ||| A lambda abstraction, of the form`\(mult binder : argTy) => retTy`, with implicitness determined by `info` + ||| A lambda abstraction, of the form`\(mult binder : argTy) => retTy`, with implicitness determined by `info` ILam : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) -> (argTy : TTImp) -> (lamTy : TTImp) -> TTImp - ||| A let binding, of the form `let mult var : nTy = nVal in scope` + ||| A let binding, of the form `let mult var : nTy = nVal in scope` ILet : FC -> (lhsFC : FC) -> (mult : Count) -> (var : Name) -> (nTy : TTImp) -> (nVal : TTImp) -> (scope : TTImp) -> TTImp - ||| A case expression `case val : ty of clauses` + ||| A case expression `case val : ty of clauses` ICase : FC -> (opts : List FnOpt) -> (val : TTImp) -> (ty : TTImp) -> (clauses : List Clause) -> TTImp - ||| A list of full declarations local to a term + ||| A list of full declarations local to a term ILocal : FC -> (context : List Decl) -> (term : TTImp) -> TTImp - ||| An update to a record value, `{ updates } val` + ||| An update to a record value, `{ updates } val` IUpdate : FC -> (updates : List IFieldUpdate) -> (val : TTImp) -> TTImp - ||| A function application, `f x` + ||| A function application, `f x` IApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp - ||| A named function application (for named parameters), e.g, `f {arg=x}` + ||| A named function application (for named parameters), e.g, `f {arg=x}` INamedApp : FC -> (f : TTImp) -> (arg : Name) -> (x : TTImp) -> TTImp - ||| An explicitly inserted auto implicit, `f @{x}` + ||| An explicitly inserted auto implicit, `f @{x}` IAutoApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp - ||| A view in a `with` rule + ||| A view in a `with` rule IWithApp : FC -> TTImp -> TTImp -> TTImp - ||| `%search` + ||| `%search` ISearch : FC -> (depth : Nat) -> TTImp ||| This operation is for expression that tries to typecheck expression in the list according to the given AltType and return either one of them, or default one (if present in the AltType), or fails IAlternative : FC -> AltType -> List TTImp -> TTImp - ||| A rewrite expression, `rewrite eq in exp` + ||| A rewrite expression, `rewrite eq in exp` IRewrite : FC -> (eq : TTImp) -> (exp : TTImp) -> TTImp ||| Any implicit bindings in the scope should be bound here, using @@ -92,7 +92,7 @@ mutual IQuote : FC -> TTImp -> TTImp ||| Quasi-quotation of a name (`{ ... }) IQuoteName : FC -> Name -> TTImp - ||| Quasi-quotation of a list of declarations (`[ ... ]) + ||| Quasi-quotation of a list of declarations (`[ ... ]) IQuoteDecl : FC -> List Decl -> TTImp ||| Unquote of an expression (~e) IUnquote : FC -> TTImp -> TTImp @@ -204,7 +204,7 @@ mutual ||| A clause in a function definition public export data Clause : Type where - ||| A simple pattern + ||| A simple pattern PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause ||| A pattern with views WithClause : FC -> (lhs : TTImp) -> @@ -212,7 +212,7 @@ mutual (prf : Maybe (Count, Name)) -> -- optional name for the proof (& quantity) (flags : List WithFlag) -> List Clause -> Clause - ||| An impossible pattern + ||| An impossible pattern ImpossibleClause : FC -> (lhs : TTImp) -> Clause %name Clause cl @@ -251,31 +251,31 @@ mutual ||| A top-level declaration public export data Decl : Type where - ||| A type ascription, `a : b`. - ||| Called a claim because of Curry Howard, the statement `x : p` is equivalent to `x` is a proof of `p`. + ||| A type ascription, `a : b`. + ||| Called a claim because of Curry Howard, the statement `x : p` is equivalent to `x` is a proof of `p`. IClaim : (claim : WithFC IClaimData) -> Decl - ||| A data declaration + ||| A data declaration IData : FC -> (vis : WithDefault Visibility Private) -> Maybe TotalReq -> (cons : Data) -> Decl - ||| A function definition by its clauses + ||| A function definition by its clauses IDef : FC -> (f : Name) -> (cls : List Clause) -> Decl - ||| A parameter block + ||| A parameter block IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) -> (decls : List Decl) -> Decl - ||| A record declaration - ||| @ ns Nested namespace + ||| A record declaration + ||| @ ns Nested namespace IRecord : FC -> (ns : Maybe String) -> (vis : WithDefault Visibility Private) -> (totality : Maybe TotalReq) -> (rec : Record) -> Decl - ||| A namespace declaration, `namespace ns where decls` + ||| A namespace declaration, `namespace ns where decls` INamespace : FC -> Namespace -> (decls : List Decl) -> Decl - ||| A transformation declaration + ||| A transformation declaration ITransform : FC -> Name -> TTImp -> TTImp -> Decl - ||| A top-level elaboration run + ||| A top-level elaboration run IRunElabDecl : FC -> TTImp -> Decl - ||| A logging directive + ||| A logging directive ILog : Maybe (List String, Nat) -> Decl - ||| A builtin declaration, `%builtin type name` + ||| A builtin declaration, `%builtin type name` IBuiltin : FC -> BuiltinType -> Name -> Decl %name Decl decl