Idris2Doc : Go.AST

Go.AST

(source)
Definitions
interface Expression : Type -> Type
  Parameters: a
Implementations:
  
Expression c => Expression v => Expression (SendStatement c v)
  
Expression t => Expression (Ellipsis t)
  
Expression f => All Expression as => Expression e => Expression (CallExpression f as e)
  
Expression BadExpression
  
Expression Identifier
  
Expression BasicLiteral
  
All Statement sts => GoType (FunctionType ts ps rs) => Expression (FunctionLiteral ts ps rs sts)
  
GoType t => All Expression es => Expression (CompositLiteral t es)
  
Expression e => Expression (ParenExpression e)
  
Expression e => Expression (SelectorExpression e)
  
GoType t => Expression e => Expression (CastExpression t e)
  
GoType t => All Expression es => Expression (MakeExpression t es)
  
Expression e => Expression i => Expression (IndexExpression e i)
  
Expression e => All Expression is => Expression (IndexListExpression e is)
  
Expression e => Expression l => Expression h => Expression m => Expression (SliceExpression e l h m)
  
Expression e => GoType t => Expression (TypeAssertExpression e t)
  
Expression e => Expression (StarExpression e)
  
Expression e => Expression (UnaryExpression e)
  
Expression x => Expression y => Expression (BinaryExpression x y)
  
Expression k => Expression v => Expression (KeyValueExpression k v)
interface Statement : Type -> Type
  Parameters: a
Implementations:
  
Statement BadStatement
  
Declaration t => Statement (DeclarationStatement t)
  
Statement EmptyStatement
  
Statement t => Statement (LabeledStatement t)
  
Expression e => Statement (ExpressionStatement e)
  
Expression e => Statement (IncDecStatement e o)
  
All Expression ls => All Expression rs => NonEmpty ls => NonEmpty rs => Statement (AssignmentStatement ls rs)
  
Expression f => All Expression as => Expression e => Statement (GoStatement f as e)
  
Expression f => All Expression as => Expression e => Statement (DeferStatement f as e)
  
All Expression rs => Statement (ReturnStatement rs)
  
Statement (BranchStatement kw)
  
All Statement sts => Statement (BlockStatement sts)
  
Statement i => Expression c => All Statement sts => Statement (IfStatement i c sts e)
  
All Expression es => NonEmpty sts => All Statement sts => Statement (CaseClause es sts)
  
Statement i => Expression e => All Statement sts => All IsCaseClause sts => Statement (SwitchStatement i e sts)
  
Statement i => Statement a => All Statement sts => Statement (TypeSwitchStatement i a sts)
  
IsSendStatement s => All Statement sts => Statement (CommClause s sts)
  
All Statement sts => Statement (SelectStatement sts)
  
Statement i => Expression c => Statement p => All Statement sts => Statement (ForStatement i c p sts)
  
Expression k => Expression v => AssignOrDefine a => Expression e => All Statement sts => Statement (KeyValueRangeStatement k v a e sts)
  
Expression v => AssignOrDefine a => Expression e => All Statement sts => Statement (ValueRangeStatement v a e sts)
  
Expression e => All Statement sts => Statement (RangeStatement e sts)
interface Specification : Type -> Type
  Parameters: a
Implementations:
  
Specification ImportSpec
  
GoType t => All Expression es => Specification (ValueSpec t es)
  
GoType t => Specification (TypeSpec ts t)
interface Declaration : Type -> Type
  Parameters: a
Implementations:
  
Declaration BadDeclaration
  
NonEmpty xs => All Specification xs => Declaration (GenericDeclaration t xs)
  
All Statement sts => Declaration (FuncDeclaration rcs ts ps rs sts)
interface GoType : Type -> Type
  Parameters: a
Implementations:
  
GoType TypeIdentifier
  
Expression l => GoType e => GoType (ArrayType l e)
  
GoType (StructType ts)
  
GoType (FunctionType ts ps rs)
  
GoType (InterfaceType ts)
  
GoType k => GoType v => GoType (MapType k v)
  
GoType e => GoType (ChanType e)
  
GoType BadType
record Comment : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkComment : String -> Comment

  Projection: 
.text : Comment -> String
.text : Comment -> String
  Totality: total
  Visibility: public export
text : Comment -> String
  Totality: total
  Visibility: public export
record CommentGroup : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCommentGroup : List1 Comment -> CommentGroup

  Projection: 
.comments : CommentGroup -> List1 Comment
.comments : CommentGroup -> List1 Comment
  Totality: total
  Visibility: public export
comments : CommentGroup -> List1 Comment
  Totality: total
  Visibility: public export
record Field : (t : Type) -> {auto 0 _ : GoType t} -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkField : Maybe CommentGroup -> List Identifier -> Maybe t -> Maybe BasicLiteral -> Maybe CommentGroup -> Field t

  Projections:
  
.comment : Field t -> Maybe CommentGroup
  
.doc : Field t -> Maybe CommentGroup
  
.names : Field t -> List Identifier
  
.tag : Field t -> Maybe BasicLiteral
  
.type : Field t -> Maybe t
.doc : Field t -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : Field t -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.names : Field t -> List Identifier
  Totality: total
  Visibility: public export
names : Field t -> List Identifier
  Totality: total
  Visibility: public export
.type : Field t -> Maybe t
  Totality: total
  Visibility: public export
type : Field t -> Maybe t
  Totality: total
  Visibility: public export
.tag : Field t -> Maybe BasicLiteral
  Totality: total
  Visibility: public export
tag : Field t -> Maybe BasicLiteral
  Totality: total
  Visibility: public export
.comment : Field t -> Maybe CommentGroup
  Totality: total
  Visibility: public export
comment : Field t -> Maybe CommentGroup
  Totality: total
  Visibility: public export
data FieldList : List Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Nil : FieldList []
  
(::) : {auto tt : GoType t} -> Field t -> FieldList ts -> FieldList (t :: ts)
record TypeIdentifier : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTypeIdentifier : Maybe Identifier -> Identifier -> TypeIdentifier

  Projections:
  
.name : TypeIdentifier -> Identifier
  
.package : TypeIdentifier -> Maybe Identifier

  Hint: 
GoType TypeIdentifier
.package : TypeIdentifier -> Maybe Identifier
  Totality: total
  Visibility: public export
package : TypeIdentifier -> Maybe Identifier
  Totality: total
  Visibility: public export
.name : TypeIdentifier -> Identifier
  Totality: total
  Visibility: public export
name : TypeIdentifier -> Identifier
  Totality: total
  Visibility: public export
record ArrayType : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkArrayType : Maybe l -> e -> ArrayType l e

  Projections:
  
.element : ArrayType l e -> e
  
.length : ArrayType l e -> Maybe l

  Hint: 
Expression l => GoType e => GoType (ArrayType l e)
.length : ArrayType l e -> Maybe l
  Totality: total
  Visibility: public export
length : ArrayType l e -> Maybe l
  Totality: total
  Visibility: public export
.element : ArrayType l e -> e
  Totality: total
  Visibility: public export
element : ArrayType l e -> e
  Totality: total
  Visibility: public export
record StructType : List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkStructType : FieldList ts -> StructType ts

  Projection: 
.fields : StructType ts -> FieldList ts

  Hint: 
GoType (StructType ts)
.fields : StructType ts -> FieldList ts
  Totality: total
  Visibility: public export
fields : StructType ts -> FieldList ts
  Totality: total
  Visibility: public export
record FunctionType : List Type -> List Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFunctionType : FieldList ts -> FieldList ps -> FieldList rs -> FunctionType ts ps rs

  Projections:
  
.params : FunctionType ts ps rs -> FieldList ps
  
.results : FunctionType ts ps rs -> FieldList rs
  
.typeParams : FunctionType ts ps rs -> FieldList ts

  Hints:
  
All Statement sts => GoType (FunctionType ts ps rs) => Expression (FunctionLiteral ts ps rs sts)
  
GoType (FunctionType ts ps rs)
.typeParams : FunctionType ts ps rs -> FieldList ts
  Totality: total
  Visibility: public export
typeParams : FunctionType ts ps rs -> FieldList ts
  Totality: total
  Visibility: public export
.params : FunctionType ts ps rs -> FieldList ps
  Totality: total
  Visibility: public export
params : FunctionType ts ps rs -> FieldList ps
  Totality: total
  Visibility: public export
.results : FunctionType ts ps rs -> FieldList rs
  Totality: total
  Visibility: public export
results : FunctionType ts ps rs -> FieldList rs
  Totality: total
  Visibility: public export
record InterfaceType : List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkInterfaceType : FieldList ts -> InterfaceType ts

  Projection: 
.methods : InterfaceType ts -> FieldList ts

  Hint: 
GoType (InterfaceType ts)
.methods : InterfaceType ts -> FieldList ts
  Totality: total
  Visibility: public export
methods : InterfaceType ts -> FieldList ts
  Totality: total
  Visibility: public export
record MapType : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkMapType : k -> v -> MapType k v

  Projections:
  
.key : MapType k v -> k
  
.value : MapType k v -> v

  Hint: 
GoType k => GoType v => GoType (MapType k v)
.key : MapType k v -> k
  Totality: total
  Visibility: public export
key : MapType k v -> k
  Totality: total
  Visibility: public export
.value : MapType k v -> v
  Totality: total
  Visibility: public export
value : MapType k v -> v
  Totality: total
  Visibility: public export
data ChanDirection : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Send : ChanDirection
  
Receive : ChanDirection
  
Both : ChanDirection
record ChanType : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkChanType : ChanDirection -> e -> ChanType e

  Projections:
  
.direction : ChanType e -> ChanDirection
  
.value : ChanType e -> e

  Hint: 
GoType e => GoType (ChanType e)
.direction : ChanType e -> ChanDirection
  Totality: total
  Visibility: public export
direction : ChanType e -> ChanDirection
  Totality: total
  Visibility: public export
.value : ChanType e -> e
  Totality: total
  Visibility: public export
value : ChanType e -> e
  Totality: total
  Visibility: public export
data BadStatement : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBadStatement : BadStatement

  Hint: 
Statement BadStatement
record DeclarationStatement : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDeclarationStatement : t -> DeclarationStatement t

  Projection: 
.declaration : DeclarationStatement t -> t

  Hint: 
Declaration t => Statement (DeclarationStatement t)
.declaration : DeclarationStatement t -> t
  Totality: total
  Visibility: public export
declaration : DeclarationStatement t -> t
  Totality: total
  Visibility: public export
record EmptyStatement : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkEmptyStatement : Bool -> EmptyStatement

  Projection: 
.isImplicit : EmptyStatement -> Bool

  Hint: 
Statement EmptyStatement
.isImplicit : EmptyStatement -> Bool
  Totality: total
  Visibility: public export
isImplicit : EmptyStatement -> Bool
  Totality: total
  Visibility: public export
record LabeledStatement : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkLabeledStatement : Identifier -> t -> LabeledStatement t

  Projections:
  
.label : LabeledStatement t -> Identifier
  
.statement : LabeledStatement t -> t

  Hint: 
Statement t => Statement (LabeledStatement t)
.label : LabeledStatement t -> Identifier
  Totality: total
  Visibility: public export
label : LabeledStatement t -> Identifier
  Totality: total
  Visibility: public export
.statement : LabeledStatement t -> t
  Totality: total
  Visibility: public export
statement : LabeledStatement t -> t
  Totality: total
  Visibility: public export
record ExpressionStatement : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkExpressionStatement : Maybe CommentGroup -> e -> Maybe CommentGroup -> ExpressionStatement e

  Projections:
  
.comment : ExpressionStatement e -> Maybe CommentGroup
  
.doc : ExpressionStatement e -> Maybe CommentGroup
  
.expression : ExpressionStatement e -> e

  Hint: 
Expression e => Statement (ExpressionStatement e)
.doc : ExpressionStatement e -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : ExpressionStatement e -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.expression : ExpressionStatement e -> e
  Totality: total
  Visibility: public export
expression : ExpressionStatement e -> e
  Totality: total
  Visibility: public export
.comment : ExpressionStatement e -> Maybe CommentGroup
  Totality: total
  Visibility: public export
comment : ExpressionStatement e -> Maybe CommentGroup
  Totality: total
  Visibility: public export
record SendStatement : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSendStatement : c -> v -> SendStatement c v

  Projections:
  
.chan : SendStatement c v -> c
  
.value : SendStatement c v -> v

  Hint: 
Expression c => Expression v => Expression (SendStatement c v)
.chan : SendStatement c v -> c
  Totality: total
  Visibility: public export
chan : SendStatement c v -> c
  Totality: total
  Visibility: public export
.value : SendStatement c v -> v
  Totality: total
  Visibility: public export
value : SendStatement c v -> v
  Totality: total
  Visibility: public export
data IncOrDec : Operator -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Inc : IncOrDec MkInc
  
Dec : IncOrDec MkDec

  Hints:
  
Show (IncOrDec MkInc)
  
Show (IncOrDec MkDec)
record IncDecStatement : Type -> Operator -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIncDecStatement : e -> IncOrDec o -> IncDecStatement e o

  Projections:
  
.expression : IncDecStatement e o -> e
  
.token : IncDecStatement e o -> IncOrDec o

  Hint: 
Expression e => Statement (IncDecStatement e o)
.expression : IncDecStatement e o -> e
  Totality: total
  Visibility: public export
expression : IncDecStatement e o -> e
  Totality: total
  Visibility: public export
.token : IncDecStatement e o -> IncOrDec o
  Totality: total
  Visibility: public export
token : IncDecStatement e o -> IncOrDec o
  Totality: total
  Visibility: public export
record AssignmentStatement : List Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkAssignmentStatement : Maybe CommentGroup -> HList ls -> Operator -> HList rs -> Maybe CommentGroup -> AssignmentStatement ls rs

  Projections:
  
.comment : AssignmentStatement ls rs -> Maybe CommentGroup
  
.doc : AssignmentStatement ls rs -> Maybe CommentGroup
  
.left : AssignmentStatement ls rs -> HList ls
  
.right : AssignmentStatement ls rs -> HList rs
  
.token : AssignmentStatement ls rs -> Operator

  Hint: 
All Expression ls => All Expression rs => NonEmpty ls => NonEmpty rs => Statement (AssignmentStatement ls rs)
.doc : AssignmentStatement ls rs -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : AssignmentStatement ls rs -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.left : AssignmentStatement ls rs -> HList ls
  Totality: total
  Visibility: public export
left : AssignmentStatement ls rs -> HList ls
  Totality: total
  Visibility: public export
.token : AssignmentStatement ls rs -> Operator
  Totality: total
  Visibility: public export
token : AssignmentStatement ls rs -> Operator
  Totality: total
  Visibility: public export
.right : AssignmentStatement ls rs -> HList rs
  Totality: total
  Visibility: public export
right : AssignmentStatement ls rs -> HList rs
  Totality: total
  Visibility: public export
.comment : AssignmentStatement ls rs -> Maybe CommentGroup
  Totality: total
  Visibility: public export
comment : AssignmentStatement ls rs -> Maybe CommentGroup
  Totality: total
  Visibility: public export
record Ellipsis : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkEllipsis : Maybe t -> Ellipsis t

  Projection: 
.elementType : Ellipsis t -> Maybe t

  Hint: 
Expression t => Expression (Ellipsis t)
.elementType : Ellipsis t -> Maybe t
  Totality: total
  Visibility: public export
elementType : Ellipsis t -> Maybe t
  Totality: total
  Visibility: public export
record CallExpression : Type -> List Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCallExpression : f -> HList as -> Maybe (Ellipsis e) -> CallExpression f as e

  Projections:
  
.args : CallExpression f as e -> HList as
  
.ellipsis : CallExpression f as e -> Maybe (Ellipsis e)
  
.function : CallExpression f as e -> f

  Hint: 
Expression f => All Expression as => Expression e => Expression (CallExpression f as e)
.function : CallExpression f as e -> f
  Totality: total
  Visibility: public export
function : CallExpression f as e -> f
  Totality: total
  Visibility: public export
.args : CallExpression f as e -> HList as
  Totality: total
  Visibility: public export
args : CallExpression f as e -> HList as
  Totality: total
  Visibility: public export
.ellipsis : CallExpression f as e -> Maybe (Ellipsis e)
  Totality: total
  Visibility: public export
ellipsis : CallExpression f as e -> Maybe (Ellipsis e)
  Totality: total
  Visibility: public export
record GoStatement : Type -> List Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkGoStatement : CallExpression f as e -> GoStatement f as e

  Projection: 
.call : GoStatement f as e -> CallExpression f as e

  Hint: 
Expression f => All Expression as => Expression e => Statement (GoStatement f as e)
.call : GoStatement f as e -> CallExpression f as e
  Totality: total
  Visibility: public export
call : GoStatement f as e -> CallExpression f as e
  Totality: total
  Visibility: public export
record DeferStatement : Type -> List Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDeferStatement : CallExpression f as e -> DeferStatement f as e

  Projection: 
.call : DeferStatement f as e -> CallExpression f as e

  Hint: 
Expression f => All Expression as => Expression e => Statement (DeferStatement f as e)
.call : DeferStatement f as e -> CallExpression f as e
  Totality: total
  Visibility: public export
call : DeferStatement f as e -> CallExpression f as e
  Totality: total
  Visibility: public export
record ReturnStatement : List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkReturnStatement : Maybe CommentGroup -> HList rs -> ReturnStatement rs

  Projections:
  
.doc : ReturnStatement rs -> Maybe CommentGroup
  
.results : ReturnStatement rs -> HList rs

  Hint: 
All Expression rs => Statement (ReturnStatement rs)
.doc : ReturnStatement rs -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : ReturnStatement rs -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.results : ReturnStatement rs -> HList rs
  Totality: total
  Visibility: public export
results : ReturnStatement rs -> HList rs
  Totality: total
  Visibility: public export
data BranchStatementToken : Keyword -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
IsBreak : BranchStatementToken MkBreak
  
IsContinue : BranchStatementToken MkContinue
  
IsGoto : BranchStatementToken MkBreak
  
IsFallthrough : BranchStatementToken MkFallthrough
record BranchStatement : Keyword -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBranchStatement : BranchStatementToken kw -> Maybe Identifier -> BranchStatement kw

  Projections:
  
.label : BranchStatement kw -> Maybe Identifier
  
.token : BranchStatement kw -> BranchStatementToken kw

  Hint: 
Statement (BranchStatement kw)
.token : BranchStatement kw -> BranchStatementToken kw
  Totality: total
  Visibility: public export
token : BranchStatement kw -> BranchStatementToken kw
  Totality: total
  Visibility: public export
.label : BranchStatement kw -> Maybe Identifier
  Totality: total
  Visibility: public export
label : BranchStatement kw -> Maybe Identifier
  Totality: total
  Visibility: public export
record BlockStatement : List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBlockStatement : HList sts -> BlockStatement sts

  Projection: 
.statements : BlockStatement sts -> HList sts

  Hint: 
All Statement sts => Statement (BlockStatement sts)
.statements : BlockStatement sts -> HList sts
  Totality: total
  Visibility: public export
statements : BlockStatement sts -> HList sts
  Totality: total
  Visibility: public export
record IfStatement : Type -> Type -> List Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIfStatement : Maybe i -> c -> BlockStatement sts -> Maybe e -> IfStatement i c sts e

  Projections:
  
.body : IfStatement i c sts e -> BlockStatement sts
  
.condition : IfStatement i c sts e -> c
  
.elseBranch : IfStatement i c sts e -> Maybe e
  
.init : IfStatement i c sts e -> Maybe i

  Hint: 
Statement i => Expression c => All Statement sts => Statement (IfStatement i c sts e)
.init : IfStatement i c sts e -> Maybe i
  Totality: total
  Visibility: public export
init : IfStatement i c sts e -> Maybe i
  Totality: total
  Visibility: public export
.condition : IfStatement i c sts e -> c
  Totality: total
  Visibility: public export
condition : IfStatement i c sts e -> c
  Totality: total
  Visibility: public export
.body : IfStatement i c sts e -> BlockStatement sts
  Totality: total
  Visibility: public export
body : IfStatement i c sts e -> BlockStatement sts
  Totality: total
  Visibility: public export
.elseBranch : IfStatement i c sts e -> Maybe e
  Totality: total
  Visibility: public export
elseBranch : IfStatement i c sts e -> Maybe e
  Totality: total
  Visibility: public export
record CaseClause : List Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCaseClause : HList es -> HList sts -> CaseClause es sts

  Projections:
  
.body : CaseClause es sts -> HList sts
  
.list : CaseClause es sts -> HList es

  Hint: 
All Expression es => NonEmpty sts => All Statement sts => Statement (CaseClause es sts)
.list : CaseClause es sts -> HList es
  Totality: total
  Visibility: public export
list : CaseClause es sts -> HList es
  Totality: total
  Visibility: public export
.body : CaseClause es sts -> HList sts
  Totality: total
  Visibility: public export
body : CaseClause es sts -> HList sts
  Totality: total
  Visibility: public export
data IsCaseClause : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsCaseClause : All Expression es => NonEmpty sts => All Statement sts => IsCaseClause (CaseClause es sts)

  Hint: 
Statement i => Expression e => All Statement sts => All IsCaseClause sts => Statement (SwitchStatement i e sts)
record SwitchStatement : Type -> Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSwitchStatement : Maybe i -> Maybe e -> BlockStatement sts -> SwitchStatement i e sts

  Projections:
  
.body : SwitchStatement i e sts -> BlockStatement sts
  
.init : SwitchStatement i e sts -> Maybe i
  
.tag : SwitchStatement i e sts -> Maybe e

  Hint: 
Statement i => Expression e => All Statement sts => All IsCaseClause sts => Statement (SwitchStatement i e sts)
.init : SwitchStatement i e sts -> Maybe i
  Totality: total
  Visibility: public export
init : SwitchStatement i e sts -> Maybe i
  Totality: total
  Visibility: public export
.tag : SwitchStatement i e sts -> Maybe e
  Totality: total
  Visibility: public export
tag : SwitchStatement i e sts -> Maybe e
  Totality: total
  Visibility: public export
.body : SwitchStatement i e sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : SwitchStatement i e sts -> BlockStatement sts
  Totality: total
  Visibility: public export
record TypeSwitchStatement : Type -> Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTypeSwitchStatement : Maybe i -> a -> BlockStatement sts -> TypeSwitchStatement i a sts

  Projections:
  
.assign : TypeSwitchStatement i a sts -> a
  
.body : TypeSwitchStatement i a sts -> BlockStatement sts
  
.init : TypeSwitchStatement i a sts -> Maybe i

  Hint: 
Statement i => Statement a => All Statement sts => Statement (TypeSwitchStatement i a sts)
.init : TypeSwitchStatement i a sts -> Maybe i
  Totality: total
  Visibility: public export
init : TypeSwitchStatement i a sts -> Maybe i
  Totality: total
  Visibility: public export
.assign : TypeSwitchStatement i a sts -> a
  Totality: total
  Visibility: public export
assign : TypeSwitchStatement i a sts -> a
  Totality: total
  Visibility: public export
.body : TypeSwitchStatement i a sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : TypeSwitchStatement i a sts -> BlockStatement sts
  Totality: total
  Visibility: public export
data IsSendStatement : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsSendStatement : Expression c => Expression v => IsSendStatement (SendStatement c v)

  Hint: 
IsSendStatement s => All Statement sts => Statement (CommClause s sts)
record CommClause : Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCommClause : Maybe s -> HList sts -> CommClause s sts

  Projections:
  
.body : CommClause s sts -> HList sts
  
.comm : CommClause s sts -> Maybe s

  Hint: 
IsSendStatement s => All Statement sts => Statement (CommClause s sts)
.comm : CommClause s sts -> Maybe s
  Totality: total
  Visibility: public export
comm : CommClause s sts -> Maybe s
  Totality: total
  Visibility: public export
.body : CommClause s sts -> HList sts
  Totality: total
  Visibility: public export
body : CommClause s sts -> HList sts
  Totality: total
  Visibility: public export
record SelectStatement : List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSelectStatement : BlockStatement sts -> SelectStatement sts

  Projection: 
.body : SelectStatement sts -> BlockStatement sts

  Hint: 
All Statement sts => Statement (SelectStatement sts)
.body : SelectStatement sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : SelectStatement sts -> BlockStatement sts
  Totality: total
  Visibility: public export
record ForStatement : Type -> Type -> Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkForStatement : Maybe i -> Maybe c -> Maybe p -> BlockStatement sts -> ForStatement i c p sts

  Projections:
  
.body : ForStatement i c p sts -> BlockStatement sts
  
.condition : ForStatement i c p sts -> Maybe c
  
.init : ForStatement i c p sts -> Maybe i
  
.post : ForStatement i c p sts -> Maybe p

  Hint: 
Statement i => Expression c => Statement p => All Statement sts => Statement (ForStatement i c p sts)
.init : ForStatement i c p sts -> Maybe i
  Totality: total
  Visibility: public export
init : ForStatement i c p sts -> Maybe i
  Totality: total
  Visibility: public export
.condition : ForStatement i c p sts -> Maybe c
  Totality: total
  Visibility: public export
condition : ForStatement i c p sts -> Maybe c
  Totality: total
  Visibility: public export
.post : ForStatement i c p sts -> Maybe p
  Totality: total
  Visibility: public export
post : ForStatement i c p sts -> Maybe p
  Totality: total
  Visibility: public export
.body : ForStatement i c p sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : ForStatement i c p sts -> BlockStatement sts
  Totality: total
  Visibility: public export
data AssignOrDefine : Operator -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
ItIsAssign : AssignOrDefine MkAssign
  
ItIsDefine : AssignOrDefine MkDefine

  Hints:
  
Show (AssignOrDefine MkAssign)
  
Show (AssignOrDefine MkDefine)
  
Expression k => Expression v => AssignOrDefine a => Expression e => All Statement sts => Statement (KeyValueRangeStatement k v a e sts)
  
Expression v => AssignOrDefine a => Expression e => All Statement sts => Statement (ValueRangeStatement v a e sts)
record KeyValueRangeStatement : Type -> Type -> Operator -> Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkKeyValueRangeStatement : k -> v -> AssignOrDefine a -> e -> BlockStatement sts -> KeyValueRangeStatement k v a e sts

  Projections:
  
.body : KeyValueRangeStatement k v a e sts -> BlockStatement sts
  
.expression : KeyValueRangeStatement k v a e sts -> e
  
.key : KeyValueRangeStatement k v a e sts -> k
  
.token : KeyValueRangeStatement k v a e sts -> AssignOrDefine a
  
.value : KeyValueRangeStatement k v a e sts -> v

  Hint: 
Expression k => Expression v => AssignOrDefine a => Expression e => All Statement sts => Statement (KeyValueRangeStatement k v a e sts)
.key : KeyValueRangeStatement k v a e sts -> k
  Totality: total
  Visibility: public export
key : KeyValueRangeStatement k v a e sts -> k
  Totality: total
  Visibility: public export
.value : KeyValueRangeStatement k v a e sts -> v
  Totality: total
  Visibility: public export
value : KeyValueRangeStatement k v a e sts -> v
  Totality: total
  Visibility: public export
.token : KeyValueRangeStatement k v a e sts -> AssignOrDefine a
  Totality: total
  Visibility: public export
token : KeyValueRangeStatement k v a e sts -> AssignOrDefine a
  Totality: total
  Visibility: public export
.expression : KeyValueRangeStatement k v a e sts -> e
  Totality: total
  Visibility: public export
expression : KeyValueRangeStatement k v a e sts -> e
  Totality: total
  Visibility: public export
.body : KeyValueRangeStatement k v a e sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : KeyValueRangeStatement k v a e sts -> BlockStatement sts
  Totality: total
  Visibility: public export
record ValueRangeStatement : Type -> Operator -> Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkValueRangeStatement : v -> AssignOrDefine a -> e -> BlockStatement sts -> ValueRangeStatement v a e sts

  Projections:
  
.body : ValueRangeStatement v a e sts -> BlockStatement sts
  
.expression : ValueRangeStatement v a e sts -> e
  
.token : ValueRangeStatement v a e sts -> AssignOrDefine a
  
.value : ValueRangeStatement v a e sts -> v

  Hint: 
Expression v => AssignOrDefine a => Expression e => All Statement sts => Statement (ValueRangeStatement v a e sts)
.value : ValueRangeStatement v a e sts -> v
  Totality: total
  Visibility: public export
value : ValueRangeStatement v a e sts -> v
  Totality: total
  Visibility: public export
.token : ValueRangeStatement v a e sts -> AssignOrDefine a
  Totality: total
  Visibility: public export
token : ValueRangeStatement v a e sts -> AssignOrDefine a
  Totality: total
  Visibility: public export
.expression : ValueRangeStatement v a e sts -> e
  Totality: total
  Visibility: public export
expression : ValueRangeStatement v a e sts -> e
  Totality: total
  Visibility: public export
.body : ValueRangeStatement v a e sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : ValueRangeStatement v a e sts -> BlockStatement sts
  Totality: total
  Visibility: public export
record RangeStatement : Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRangeStatement : e -> BlockStatement sts -> RangeStatement e sts

  Projections:
  
.body : RangeStatement e sts -> BlockStatement sts
  
.expression : RangeStatement e sts -> e

  Hint: 
Expression e => All Statement sts => Statement (RangeStatement e sts)
.expression : RangeStatement e sts -> e
  Totality: total
  Visibility: public export
expression : RangeStatement e sts -> e
  Totality: total
  Visibility: public export
.body : RangeStatement e sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : RangeStatement e sts -> BlockStatement sts
  Totality: total
  Visibility: public export
data BadExpression : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBadExpression : BadExpression

  Hint: 
Expression BadExpression
record Identifier : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIdentifier : String -> Identifier

  Projection: 
.name : Identifier -> String

  Hint: 
Expression Identifier
.name : Identifier -> String
  Totality: total
  Visibility: public export
name : Identifier -> String
  Totality: total
  Visibility: public export
record BasicLiteral : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBasicLiteral : Literal -> String -> BasicLiteral

  Projections:
  
.kind : BasicLiteral -> Literal
  
.value : BasicLiteral -> String

  Hint: 
Expression BasicLiteral
.kind : BasicLiteral -> Literal
  Totality: total
  Visibility: public export
kind : BasicLiteral -> Literal
  Totality: total
  Visibility: public export
.value : BasicLiteral -> String
  Totality: total
  Visibility: public export
value : BasicLiteral -> String
  Totality: total
  Visibility: public export
record FunctionLiteral : List Type -> List Type -> List Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFunctionLiteral : FunctionType ts ps rs -> BlockStatement sts -> FunctionLiteral ts ps rs sts

  Projections:
  
.body : FunctionLiteral ts ps rs sts -> BlockStatement sts
  
.type : FunctionLiteral ts ps rs sts -> FunctionType ts ps rs

  Hint: 
All Statement sts => GoType (FunctionType ts ps rs) => Expression (FunctionLiteral ts ps rs sts)
.type : FunctionLiteral ts ps rs sts -> FunctionType ts ps rs
  Totality: total
  Visibility: public export
type : FunctionLiteral ts ps rs sts -> FunctionType ts ps rs
  Totality: total
  Visibility: public export
.body : FunctionLiteral ts ps rs sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : FunctionLiteral ts ps rs sts -> BlockStatement sts
  Totality: total
  Visibility: public export
record CompositLiteral : Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCompositLiteral : Maybe t -> HList es -> CompositLiteral t es

  Projections:
  
.expressions : CompositLiteral t es -> HList es
  
.type : CompositLiteral t es -> Maybe t

  Hint: 
GoType t => All Expression es => Expression (CompositLiteral t es)
.type : CompositLiteral t es -> Maybe t
  Totality: total
  Visibility: public export
type : CompositLiteral t es -> Maybe t
  Totality: total
  Visibility: public export
.expressions : CompositLiteral t es -> HList es
  Totality: total
  Visibility: public export
expressions : CompositLiteral t es -> HList es
  Totality: total
  Visibility: public export
record ParenExpression : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkParenExpression : e -> ParenExpression e

  Projection: 
.expression : ParenExpression e -> e

  Hint: 
Expression e => Expression (ParenExpression e)
.expression : ParenExpression e -> e
  Totality: total
  Visibility: public export
expression : ParenExpression e -> e
  Totality: total
  Visibility: public export
record SelectorExpression : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSelectorExpression : e -> Identifier -> SelectorExpression e

  Projections:
  
.expression : SelectorExpression e -> e
  
.selector : SelectorExpression e -> Identifier

  Hint: 
Expression e => Expression (SelectorExpression e)
.expression : SelectorExpression e -> e
  Totality: total
  Visibility: public export
expression : SelectorExpression e -> e
  Totality: total
  Visibility: public export
.selector : SelectorExpression e -> Identifier
  Totality: total
  Visibility: public export
selector : SelectorExpression e -> Identifier
  Totality: total
  Visibility: public export
record CastExpression : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCastExpression : t -> e -> CastExpression t e

  Projections:
  
.expression : CastExpression t e -> e
  
.type : CastExpression t e -> t

  Hint: 
GoType t => Expression e => Expression (CastExpression t e)
.type : CastExpression t e -> t
  Totality: total
  Visibility: public export
type : CastExpression t e -> t
  Totality: total
  Visibility: public export
.expression : CastExpression t e -> e
  Totality: total
  Visibility: public export
expression : CastExpression t e -> e
  Totality: total
  Visibility: public export
record MakeExpression : Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkMakeExpression : t -> HList es -> MakeExpression t es

  Projections:
  
.expressions : MakeExpression t es -> HList es
  
.type : MakeExpression t es -> t

  Hint: 
GoType t => All Expression es => Expression (MakeExpression t es)
.type : MakeExpression t es -> t
  Totality: total
  Visibility: public export
type : MakeExpression t es -> t
  Totality: total
  Visibility: public export
.expressions : MakeExpression t es -> HList es
  Totality: total
  Visibility: public export
expressions : MakeExpression t es -> HList es
  Totality: total
  Visibility: public export
record IndexExpression : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIndexExpression : e -> i -> IndexExpression e i

  Projections:
  
.expression : IndexExpression e i -> e
  
.index : IndexExpression e i -> i

  Hint: 
Expression e => Expression i => Expression (IndexExpression e i)
.expression : IndexExpression e i -> e
  Totality: total
  Visibility: public export
expression : IndexExpression e i -> e
  Totality: total
  Visibility: public export
.index : IndexExpression e i -> i
  Totality: total
  Visibility: public export
index : IndexExpression e i -> i
  Totality: total
  Visibility: public export
record IndexListExpression : Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIndexListExpression : e -> HList is -> IndexListExpression e is

  Projections:
  
.expression : IndexListExpression e is -> e
  
.indices : IndexListExpression e is -> HList is

  Hint: 
Expression e => All Expression is => Expression (IndexListExpression e is)
.expression : IndexListExpression e is -> e
  Totality: total
  Visibility: public export
expression : IndexListExpression e is -> e
  Totality: total
  Visibility: public export
.indices : IndexListExpression e is -> HList is
  Totality: total
  Visibility: public export
indices : IndexListExpression e is -> HList is
  Totality: total
  Visibility: public export
record SliceExpression : Type -> Type -> Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkSliceExpression : e -> Maybe l -> Maybe h -> Maybe m -> SliceExpression e l h m

  Projections:
  
.expression : SliceExpression e l h m -> e
  
.high : SliceExpression e l h m -> Maybe h
  
.low : SliceExpression e l h m -> Maybe l
  
.max : SliceExpression e l h m -> Maybe m

  Hint: 
Expression e => Expression l => Expression h => Expression m => Expression (SliceExpression e l h m)
.expression : SliceExpression e l h m -> e
  Totality: total
  Visibility: public export
expression : SliceExpression e l h m -> e
  Totality: total
  Visibility: public export
.low : SliceExpression e l h m -> Maybe l
  Totality: total
  Visibility: public export
low : SliceExpression e l h m -> Maybe l
  Totality: total
  Visibility: public export
.high : SliceExpression e l h m -> Maybe h
  Totality: total
  Visibility: public export
high : SliceExpression e l h m -> Maybe h
  Totality: total
  Visibility: public export
.max : SliceExpression e l h m -> Maybe m
  Totality: total
  Visibility: public export
max : SliceExpression e l h m -> Maybe m
  Totality: total
  Visibility: public export
record TypeAssertExpression : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTypeAssertExpression : e -> t -> TypeAssertExpression e t

  Projections:
  
.expression : TypeAssertExpression e t -> e
  
.type : TypeAssertExpression e t -> t

  Hint: 
Expression e => GoType t => Expression (TypeAssertExpression e t)
.expression : TypeAssertExpression e t -> e
  Totality: total
  Visibility: public export
expression : TypeAssertExpression e t -> e
  Totality: total
  Visibility: public export
.type : TypeAssertExpression e t -> t
  Totality: total
  Visibility: public export
type : TypeAssertExpression e t -> t
  Totality: total
  Visibility: public export
record StarExpression : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkStarExpression : e -> StarExpression e

  Projection: 
.expression : StarExpression e -> e

  Hint: 
Expression e => Expression (StarExpression e)
.expression : StarExpression e -> e
  Totality: total
  Visibility: public export
expression : StarExpression e -> e
  Totality: total
  Visibility: public export
record UnaryExpression : Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkUnaryExpression : Operator -> e -> UnaryExpression e

  Projections:
  
.expression : UnaryExpression e -> e
  
.operator : UnaryExpression e -> Operator

  Hint: 
Expression e => Expression (UnaryExpression e)
.operator : UnaryExpression e -> Operator
  Totality: total
  Visibility: public export
operator : UnaryExpression e -> Operator
  Totality: total
  Visibility: public export
.expression : UnaryExpression e -> e
  Totality: total
  Visibility: public export
expression : UnaryExpression e -> e
  Totality: total
  Visibility: public export
record BinaryExpression : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBinaryExpression : x -> Operator -> y -> BinaryExpression x y

  Projections:
  
.first : BinaryExpression x y -> x
  
.last : BinaryExpression x y -> y
  
.operator : BinaryExpression x y -> Operator

  Hint: 
Expression x => Expression y => Expression (BinaryExpression x y)
.first : BinaryExpression x y -> x
  Totality: total
  Visibility: public export
first : BinaryExpression x y -> x
  Totality: total
  Visibility: public export
.operator : BinaryExpression x y -> Operator
  Totality: total
  Visibility: public export
operator : BinaryExpression x y -> Operator
  Totality: total
  Visibility: public export
.last : BinaryExpression x y -> y
  Totality: total
  Visibility: public export
last : BinaryExpression x y -> y
  Totality: total
  Visibility: public export
record KeyValueExpression : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkKeyValueExpression : k -> v -> KeyValueExpression k v

  Projections:
  
.key : KeyValueExpression k v -> k
  
.value : KeyValueExpression k v -> v

  Hint: 
Expression k => Expression v => Expression (KeyValueExpression k v)
.key : KeyValueExpression k v -> k
  Totality: total
  Visibility: public export
key : KeyValueExpression k v -> k
  Totality: total
  Visibility: public export
.value : KeyValueExpression k v -> v
  Totality: total
  Visibility: public export
value : KeyValueExpression k v -> v
  Totality: total
  Visibility: public export
record ImportSpec : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkImportSpec : Maybe CommentGroup -> Maybe Identifier -> BasicLiteral -> Maybe CommentGroup -> ImportSpec

  Projections:
  
.comment : ImportSpec -> Maybe CommentGroup
  
.doc : ImportSpec -> Maybe CommentGroup
  
.name : ImportSpec -> Maybe Identifier
  
.path : ImportSpec -> BasicLiteral

  Hint: 
Specification ImportSpec
.doc : ImportSpec -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : ImportSpec -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.name : ImportSpec -> Maybe Identifier
  Totality: total
  Visibility: public export
name : ImportSpec -> Maybe Identifier
  Totality: total
  Visibility: public export
.path : ImportSpec -> BasicLiteral
  Totality: total
  Visibility: public export
path : ImportSpec -> BasicLiteral
  Totality: total
  Visibility: public export
.comment : ImportSpec -> Maybe CommentGroup
  Totality: total
  Visibility: public export
comment : ImportSpec -> Maybe CommentGroup
  Totality: total
  Visibility: public export
record ValueSpec : Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkValueSpec : Maybe CommentGroup -> List1 Identifier -> Maybe t -> HList es -> Maybe CommentGroup -> ValueSpec t es

  Projections:
  
.comment : ValueSpec t es -> Maybe CommentGroup
  
.doc : ValueSpec t es -> Maybe CommentGroup
  
.names : ValueSpec t es -> List1 Identifier
  
.type : ValueSpec t es -> Maybe t
  
.values : ValueSpec t es -> HList es

  Hint: 
GoType t => All Expression es => Specification (ValueSpec t es)
.doc : ValueSpec t es -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : ValueSpec t es -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.names : ValueSpec t es -> List1 Identifier
  Totality: total
  Visibility: public export
names : ValueSpec t es -> List1 Identifier
  Totality: total
  Visibility: public export
.type : ValueSpec t es -> Maybe t
  Totality: total
  Visibility: public export
type : ValueSpec t es -> Maybe t
  Totality: total
  Visibility: public export
.values : ValueSpec t es -> HList es
  Totality: total
  Visibility: public export
values : ValueSpec t es -> HList es
  Totality: total
  Visibility: public export
.comment : ValueSpec t es -> Maybe CommentGroup
  Totality: total
  Visibility: public export
comment : ValueSpec t es -> Maybe CommentGroup
  Totality: total
  Visibility: public export
record TypeSpec : List Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTypeSpec : Maybe CommentGroup -> Identifier -> FieldList ts -> t -> Maybe CommentGroup -> TypeSpec ts t

  Projections:
  
.comment : TypeSpec ts t -> Maybe CommentGroup
  
.doc : TypeSpec ts t -> Maybe CommentGroup
  
.name : TypeSpec ts t -> Identifier
  
.type : TypeSpec ts t -> t
  
.typeParams : TypeSpec ts t -> FieldList ts

  Hint: 
GoType t => Specification (TypeSpec ts t)
.doc : TypeSpec ts t -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : TypeSpec ts t -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.name : TypeSpec ts t -> Identifier
  Totality: total
  Visibility: public export
name : TypeSpec ts t -> Identifier
  Totality: total
  Visibility: public export
.typeParams : TypeSpec ts t -> FieldList ts
  Totality: total
  Visibility: public export
typeParams : TypeSpec ts t -> FieldList ts
  Totality: total
  Visibility: public export
.type : TypeSpec ts t -> t
  Totality: total
  Visibility: public export
type : TypeSpec ts t -> t
  Totality: total
  Visibility: public export
.comment : TypeSpec ts t -> Maybe CommentGroup
  Totality: total
  Visibility: public export
comment : TypeSpec ts t -> Maybe CommentGroup
  Totality: total
  Visibility: public export
data BadDeclaration : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBadDeclaration : BadDeclaration

  Hint: 
Declaration BadDeclaration
data GenericDeclarationToken : Keyword -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Import : GenericDeclarationToken MkImport
  
Const : GenericDeclarationToken MkConst
  
Type' : GenericDeclarationToken MkType
  
Var : GenericDeclarationToken MkVar

  Hints:
  
Show (GenericDeclarationToken MkImport)
  
Show (GenericDeclarationToken MkConst)
  
Show (GenericDeclarationToken MkType)
  
Show (GenericDeclarationToken MkVar)
record GenericDeclaration : Keyword -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkGenericDeclaration : Maybe CommentGroup -> GenericDeclarationToken t -> HList xs -> GenericDeclaration t xs

  Projections:
  
.doc : GenericDeclaration t xs -> Maybe CommentGroup
  
.specs : GenericDeclaration t xs -> HList xs
  
.token : GenericDeclaration t xs -> GenericDeclarationToken t

  Hint: 
NonEmpty xs => All Specification xs => Declaration (GenericDeclaration t xs)
.doc : GenericDeclaration t xs -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : GenericDeclaration t xs -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.token : GenericDeclaration t xs -> GenericDeclarationToken t
  Totality: total
  Visibility: public export
token : GenericDeclaration t xs -> GenericDeclarationToken t
  Totality: total
  Visibility: public export
.specs : GenericDeclaration t xs -> HList xs
  Totality: total
  Visibility: public export
specs : GenericDeclaration t xs -> HList xs
  Totality: total
  Visibility: public export
record FuncDeclaration : List Type -> List Type -> List Type -> List Type -> List Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFuncDeclaration : Maybe CommentGroup -> FieldList rcs -> Identifier -> FunctionType ts ps rs -> BlockStatement sts -> FuncDeclaration rcs ts ps rs sts

  Projections:
  
.body : FuncDeclaration rcs ts ps rs sts -> BlockStatement sts
  
.doc : FuncDeclaration rcs ts ps rs sts -> Maybe CommentGroup
  
.name : FuncDeclaration rcs ts ps rs sts -> Identifier
  
.reciever : FuncDeclaration rcs ts ps rs sts -> FieldList rcs
  
.type : FuncDeclaration rcs ts ps rs sts -> FunctionType ts ps rs

  Hint: 
All Statement sts => Declaration (FuncDeclaration rcs ts ps rs sts)
.doc : FuncDeclaration rcs ts ps rs sts -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : FuncDeclaration rcs ts ps rs sts -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.reciever : FuncDeclaration rcs ts ps rs sts -> FieldList rcs
  Totality: total
  Visibility: public export
reciever : FuncDeclaration rcs ts ps rs sts -> FieldList rcs
  Totality: total
  Visibility: public export
.name : FuncDeclaration rcs ts ps rs sts -> Identifier
  Totality: total
  Visibility: public export
name : FuncDeclaration rcs ts ps rs sts -> Identifier
  Totality: total
  Visibility: public export
.type : FuncDeclaration rcs ts ps rs sts -> FunctionType ts ps rs
  Totality: total
  Visibility: public export
type : FuncDeclaration rcs ts ps rs sts -> FunctionType ts ps rs
  Totality: total
  Visibility: public export
.body : FuncDeclaration rcs ts ps rs sts -> BlockStatement sts
  Totality: total
  Visibility: public export
body : FuncDeclaration rcs ts ps rs sts -> BlockStatement sts
  Totality: total
  Visibility: public export
record File : (ds : List Type) -> {auto 0 _ : All Declaration ds} -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFile : Maybe CommentGroup -> String -> Identifier -> HList ds -> List ImportSpec -> List Identifier -> List CommentGroup -> File ds

  Projections:
  
.comments : File ds -> List CommentGroup
  
.decls : File ds -> HList ds
  
.doc : File ds -> Maybe CommentGroup
  
.imports : File ds -> List ImportSpec
  
.name : File ds -> String
  
.packageName : File ds -> Identifier
  
.unresolved : File ds -> List Identifier
.doc : File ds -> Maybe CommentGroup
  Totality: total
  Visibility: public export
doc : File ds -> Maybe CommentGroup
  Totality: total
  Visibility: public export
.name : File ds -> String
  Totality: total
  Visibility: public export
name : File ds -> String
  Totality: total
  Visibility: public export
.packageName : File ds -> Identifier
  Totality: total
  Visibility: public export
packageName : File ds -> Identifier
  Totality: total
  Visibility: public export
.decls : File ds -> HList ds
  Totality: total
  Visibility: public export
decls : File ds -> HList ds
  Totality: total
  Visibility: public export
.imports : File ds -> List ImportSpec
  Totality: total
  Visibility: public export
imports : File ds -> List ImportSpec
  Totality: total
  Visibility: public export
.unresolved : File ds -> List Identifier
  Totality: total
  Visibility: public export
unresolved : File ds -> List Identifier
  Totality: total
  Visibility: public export
.comments : File ds -> List CommentGroup
  Totality: total
  Visibility: public export
comments : File ds -> List CommentGroup
  Totality: total
  Visibility: public export
data BadType : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBadType : BadType

  Hint: 
GoType BadType