Types
AgdaNodeKind = enum agdaAbstract, ## abstract agdaAtom, ## atom agdaAttribute, ## attribute agdaAttributes, ## attributes agdaBid, ## bid agdaCatchallPragma, ## catchall_pragma agdaData, ## data agdaDataName, ## data_name agdaDataSignature, ## data_signature agdaDo, ## do agdaDoWhere, ## do_where agdaExpr, ## expr agdaFieldAssignment, ## field_assignment agdaFields, ## fields agdaForall, ## forall agdaFunction, ## function agdaFunctionName, ## function_name agdaGeneralize, ## generalize agdaHoleName, ## hole_name agdaHoleNames, ## hole_names agdaImportDirective, ## import_directive agdaInfix, ## infix agdaInstance, ## instance agdaInteger, ## integer agdaLambda, ## lambda agdaLambdaClause, ## lambda_clause agdaLambdaClauseAbsurd, ## lambda_clause_absurd agdaLet, ## let agdaLhs, ## lhs agdaLiteral, ## literal agdaMacro, ## macro agdaModule, ## module agdaModuleApplication, ## module_application agdaModuleAssignment, ## module_assignment agdaModuleMacro, ## module_macro agdaModuleName, ## module_name agdaMutual, ## mutual agdaOpen, ## open agdaPattern, ## pattern agdaPostulate, ## postulate agdaPrimitive, ## primitive agdaPrivate, ## private agdaQid, ## qid agdaRecord, ## record agdaRecordAssignments, ## record_assignments agdaRecordConstructor, ## record_constructor agdaRecordConstructorInstance, ## record_constructor_instance agdaRecordDeclarationsBlock, ## record_declarations_block agdaRecordEta, ## record_eta agdaRecordInduction, ## record_induction agdaRecordName, ## record_name agdaRecordSignature, ## record_signature agdaRenaming, ## renaming agdaRewriteEquations, ## rewrite_equations agdaRhs, ## rhs agdaSignature, ## signature agdaSourceFile, ## source_file agdaStmt, ## stmt agdaSyntax, ## syntax agdaTypeSignature, ## type_signature agdaTypedBinding, ## typed_binding agdaUnquoteDecl, ## unquote_decl agdaUntypedBinding, ## untyped_binding agdaWhere, ## where agdaWithExpressions, ## with_expressions agdaHashMinusRCurlyTok, ## #-} agdaLParTok, ## ( agdaLParPipeTok, ## (| agdaRParTok, ## ) agdaMinusTok, ## - agdaDotTok, ## . agdaDoubleDotTok, ## .. agdaColonTok, ## : agdaSemicolonTok, ## ; agdaEqualTok, ## = agdaAtTok, ## @ agdaCATCHALLTok, ## CATCHALL agdaPropTok, ## Prop agdaPropN, ## PropN agdaSetTok, ## Set agdaSetN, ## SetN agdaUnderscoreTok, ## _ agdaAbstractTok, ## abstract agdaBidTok, ## bid agdaCodataTok, ## codata agdaCoinductiveTok, ## coinductive agdaComment, ## comment agdaConstructorTok, ## constructor agdaDataTok, ## data agdaDataNameTok, ## data_name agdaDoTok, ## do agdaEtaMinusequalityTok, ## eta-equality agdaFieldTok, ## field agdaFieldName, ## field_name agdaHidingTok, ## hiding agdaId, ## id agdaImportTok, ## import agdaInTok, ## in agdaInductiveTok, ## inductive agdaInfixTok, ## infix agdaInfixlTok, ## infixl agdaInfixrTok, ## infixr agdaInstanceTok, ## instance agdaLetTok, ## let agdaMacroTok, ## macro agdaModuleTok, ## module agdaMutualTok, ## mutual agdaNoMinusetaMinusequalityTok, ## no-eta-equality agdaOpenTok, ## open agdaOverlapTok, ## overlap agdaPatternTok, ## pattern agdaPostulateTok, ## postulate agdaPragma, ## pragma agdaPrimitiveTok, ## primitive agdaPrivateTok, ## private agdaPublicTok, ## public agdaQidTok, ## qid agdaQuoteTok, ## quote agdaQuoteContextTok, ## quoteContext agdaQuoteGoalTok, ## quoteGoal agdaQuoteTermTok, ## quoteTerm agdaRecordTok, ## record agdaRenamingTok, ## renaming agdaRewriteTok, ## rewrite agdaSyntaxTok, ## syntax agdaTacticTok, ## tactic agdaToTok, ## to agdaUnquoteTok, ## unquote agdaUnquoteDeclTok, ## unquoteDecl agdaUnquoteDefTok, ## unquoteDef agdaUsingTok, ## using agdaVariableTok, ## variable agdaWhereTok, ## where agdaWithTok, ## with agdaLCurlyTok, ## { agdaLCurlyMinusHashTok, ## {-# agdaDoubleLCurlyTok, ## {{ agdaPipeTok, ## | agdaPipeRParTok, ## |) agdaRCurlyTok, ## } agdaDoubleRCurlyTok, ## }} agda⦃Tok, ## ⦃ agda⦄Tok, ## ⦄ agda⦇Tok, ## ⦇ agda⦈Tok, ## ⦈ agdaSyntaxError ## Tree-sitter parser syntax error
AgdaExternalTok = enum agdaExtern_newline, ## _newline agdaExtern_indent, ## _indent agdaExtern_dedent ## _dedent
TsAgdaNode = distinct TSNode
AgdaParser = distinct PtsParser
AgdaNode = HtsNode[TsAgdaNode, AgdaNodeKind]
Procs
proc kind(node: TsAgdaNode): AgdaNodeKind {...}{.noSideEffect, raises: [Exception], tags: [RootEffect].}
proc tsNodeType(node: TsAgdaNode): string {...}{.raises: [], tags: [].}
proc newTsAgdaParser(): AgdaParser {...}{.raises: [], tags: [].}
proc parseString(parser: AgdaParser; str: string): TsAgdaNode {...}{.raises: [], tags: [].}
proc parseTsAgdaString(str: string): TsAgdaNode {...}{.raises: [], tags: [].}
proc treeReprTsAgda(str: string; unnamed: bool = false): string {...}{. raises: [ValueError, Exception, NilArgumentError], tags: [RootEffect].}
proc toHtsNode(node: TsAgdaNode; str: ptr string): HtsNode[TsAgdaNode, AgdaNodeKind] {...}{.raises: [NilArgumentError, Exception], tags: [RootEffect].}
proc toHtsTree(node: TsAgdaNode; str: ptr string): AgdaNode {...}{. raises: [NilArgumentError, Exception], tags: [RootEffect].}
proc parseAgdaString(str: ptr string; unnamed: bool = false): AgdaNode {...}{. raises: [NilArgumentError, Exception], tags: [RootEffect].}
proc parseAgdaString(str: string; unnamed: bool = false): AgdaNode {...}{. raises: [NilArgumentError, Exception], tags: [RootEffect].}
Funcs
func isNil(node: TsAgdaNode): bool {...}{.raises: [], tags: [].}
func len(node: TsAgdaNode; unnamed: bool = false): int {...}{.raises: [], tags: [].}
func has(node: TsAgdaNode; idx: int; unnamed: bool = false): bool {...}{.raises: [], tags: [].}
func `$`(node: TsAgdaNode): string {...}{.raises: [Exception], tags: [RootEffect].}
func `[]`(node: TsAgdaNode; idx: int; kind: AgdaNodeKind | set[AgdaNodeKind]): TsAgdaNode