agda2train-0.0.3.0: Agda backend to generate training data for machine learning purposes. (Index)

agda2train-0.0.3.0: Agda backend to generate training data for machine learning purposes.

Index

:>	Output
:~	Output
ADT	Output
App	Output
body	Output
C	ToTrain
Clause
1 (Type/Class)	Output
2 (Data Constructor)	Output
clauses	Output
Constructor	Output
convert	Output
ctx	Output
DB	Output
Definition	Output
definition	Output
defsToSkip	ToTrain
fields	Output
FileData	Output
forEachHole	ToTrain
Function	Output
go	Output
goal	Output
Head	Output
holes	Output
isNotCubical	Output
item	Output
jsonOpts	Output
Lam	Output
Level	Output
Lit	Output
maxDuration	ToTrain
mkReduced	ToTrain
Name	Output
name	Output
Named
1 (Type/Class)	Output
2 (Data Constructor)	Output
names	ToTrain
noop	ToTrain
normalised	Output
original	Output
panic	Output
Pattern	Output
patterns	Output
pbindings	Output
Pi	Output
pinterleave	Output
Postulate	Output
pp	Output
ppm	Output
ppName	Output
premises	Output
prender	Output
Pretty
1 (Type/Class)	Output
2 (Data Constructor)	Output
pretty	Output
Primitive	Output
Record	Output
Reduced
1 (Type/Class)	Output
2 (Data Constructor)	Output
reduced	Output
reference	Output
report	Output
reportReduced	ToTrain
runC	ToTrain
Sample
1 (Type/Class)	Output
2 (Data Constructor)	Output
ScopeEntry
1 (Data Constructor)	Output
2 (Type/Class)	Output
ScopeEntry'	Output
scopeGlobal	Output
scopeLocal	Output
scopePrivate	Output
silently	ToTrain
simplified	Output
Sort	Output
Telescope	Output
telescope	Output
Term	Output
term	Output
thing	Output
train	ToTrain
TrainData
1 (Type/Class)	Output
2 (Data Constructor)	Output
TrainF	ToTrain
Type	Output
unqualify	Output
UnsolvedMeta	Output
variant	Output
variants	Output
withTimeout	ToTrain
\/	Output
_telescope	Output
_type	Output
~>	Output