Skip to content

Instantly share code, notes, and snippets.

@mpickering
Created April 9, 2024 11:09
Show Gist options
  • Save mpickering/3cacb2f5364f26edfbfd754825a6669a to your computer and use it in GitHub Desktop.
Save mpickering/3cacb2f5364f26edfbfd754825a6669a to your computer and use it in GitHub Desktop.
6 Type
6 TyCon
6 CallStack
8 Addr#
8 TrName
11 b1
15 'Lifted
29 Int
48 'Many
76 AgdaError
total (47, 281)
--
4 String
5 Addr#
5 Char
5 TrName
5 KindRep
6 b
6 CutOff -> CutOff -> Bool
8 Int
44 'Many
45 CutOff
total (37, 172)
--
4 TyCon
5 Semiring a
6 Addr#
6 TrName
7 Int
7 Integer
9 a
9 'Many
11 Type
15 KindRep
total (27, 104)
--
6 Addr#
6 TrName
9 AffineHole r b
10 AffineHole r a
11 KindRep
18 a
22 b
35 'Many
38 r
55 Type
total (63, 285)
--
6 f b
7 b
7 t
8 Alternative f
10 f a
16 Type -> Type
18 a
20 f
22 Type
36 'Many
total (57, 222)
--
14 Boolean b
19 KindRep
21 a -> b
23 IsBool a
31 Bool
31 Boolean a
37 b
76 Type
87 a
123 'Many
total (70, 577)
--
18 C
23 U1 @Type
24 Int
25 Bool
31 x
34 'Lifted
63 Type
69 IsFibrant
136 'Many
136 Univ
total (134, 868)
--
5 Char
5 Word
5 HasCallStack
6 "callStack"
7 String
7 [Char]
7 CallSite
13 Type
26 'Many
28 CallStack
total (42, 168)
--
1 Integer -> Integer
1 Bool
1 Module
1 GeneralCategory
2 Addr#
2 TrName
3 Int
8 'Many
11 Char
12 Integer
total (14, 46)
--
6 EnvVars
6 (String, String)
9 KindRep
12 [Char]
18 [Token]
20 LiftedRep
27 Char
32 Token
36 String
46 'Many
total (53, 292)
--
9 String
10 Either String
10 Fail a
12 [Char]
12 Either String a
15 KindRep
22 b
44 a
48 'Many
85 Type
total (72, 364)
--
12 Bool
13 (Bool, a)
14 LiftedRep
16 m
17 i
18 a -> a
31 b
48 Type
60 a
96 'Many
total (93, 495)
--
8 LiftedRep
8 TyCon
10 Addr#
10 Bool
10 Int
10 TrName
24 Type
27 a
30 'Many
34 KindRep
total (46, 250)
--
15 d
21 Decoration t
22 Functor m
25 b
28 m
30 t
37 a
52 Type -> Type
68 Type
100 'Many
total (153, 632)
--
6 Eq k
6 Hashable k
9 IO
9 Set k
10 HashTable k v
18 MVector
22 v
25 Type
28 'Many
33 k
total (57, 222)
--
33 ModuleName
46 LiftedRep
46 ()
74 Bool
87 TyCon
89 Addr#
89 TrName
99 'One
138 'Many
207 KindRep
total (147, 1491)
--
8 Stmt
8 Match
8 GuardedRhs
9 MakeStrict a
10 Pat
10 Binds
10 Decl
12 a
12 Type
39 'Many
total (70, 237)
--
5 WriterT w m a
6 w
7 IOException
8 s
9 CatchIO m
12 Type -> Type
13 a
17 m
19 Type
34 'Many
total (58, 204)
--
1 Module
1 ()
2 Addr#
2 TrName
2 FilePath
2 Handle
3 IO
3 ByteString
4 'Many
4 (ByteString, IO ())
total (13, 27)
--
9 WriterT (Endo [CopyDirAction]) IO
9 CopyDirAction
10 KindRep
11 [CopyDirAction]
12 LiftedRep
14 ()
16 IO
16 Endo [CopyDirAction]
19 FilePath
21 'Many
total (38, 202)
--
2 String
2 LiftedRep
2 TrName
3 IO FilePath
3 Handle
4 IO
4 ()
4 (FilePath, Handle)
5 'Many
10 FilePath
total (15, 45)
--
8 Char
8 ByteString
9 KindRep
11 String
11 Type
11 LiftedRep
11 FilePath
16 Text
26 ReadException
38 'Many
total (61, 251)
--
1 Module
2 a -> a
2 Addr#
2 Type
2 TrName
2 IORef a
2 ()
3 IO
6 'Many
12 a
total (16, 40)
--
15 String
16 CatchImpossible m
17 Type -> Type
17 KindRep
19 CallStack
20 m a
26 a
50 Type
75 Impossible
102 'Many
total (113, 594)
--
3 Int
3 Type
3 TrName
4 ShowS
5 IO
6 Empty -> Empty -> Bool
7 Maybe Impossible
8 Impossible
41 'Many
47 Empty
total (40, 165)
--
8 b1
8 BoolSet -> BoolSet -> Bool
8 CallStack
9 BoolSet -> BoolSet -> BoolSet
11 LiftedRep
22 Int
30 'Lifted
41 Bool
88 'Many
134 BoolSet
total (57, 465)
--
19 Bool
30 m
40 Ord a
50 Map a [a]
51 [a]
89 b
111 Bag a
134 Type
256 a
296 'Many
total (243, 1573)
--
10 [Integer]
11 KindRep
13 (Maybe Integer, Maybe Integer, Set Integer)
18 Set Integer
23 String
27 LiftedRep
43 b
92 IntSet
99 'Many
116 Integer
total (72, 596)
--
12 MonadState o m
13 a
20 r
24 Lens' o i
27 Type -> Type
58 m
58 o
66 i
94 Type
128 'Many
total (171, 798)
--
18 x -> Type
19 xs
20 p
24 [x]
30 x1
31 [KindRep]
44 Type
52 'Many
72 x
74 KindRep
total (131, 679)
--
4 Functor f
4 Addr#
4 TrName
6 f
9 a
9 b
9 KindRep
10 Record a b
20 'Many
23 Type
total (37, 134)
--
4 Bool
4 Maybe v
6 (,) a
7 Map k v
8 a
11 k
14 f
14 v
26 Type
30 'Many
total (57, 195)
--
13 m b
16 m (Maybe a)
16 Monad m
18 Type -> Type
23 b
26 Maybe a
28 m
55 a
58 Type
113 'Many
total (133, 559)
--
6 HashMap a b
9 s
10 Maybe a
12 IO
13 a -> b
18 Type
24 b
25 m
37 a
39 'Many
total (53, 280)
--
5 KindRep
6 Int -> Int -> Bool
6 Int -> Int -> Int
7 Bool
8 Int -> Int
11 String
39 MaxNat
43 b
45 Int
87 'Many
total (60, 338)
--
24 Null (m a)
28 b
31 m
32 Bool
36 Type -> Type
36 Monad m
53 Null a
119 a
200 Type
239 'Many
total (346, 1374)
--
12 Type -> Type
12 Monad m
12 Maybe b
13 m
13 m b
29 b
29 Maybe a
42 a
60 Type
101 'Many
total (122, 500)
--
19 PartialOrd a
20 Inclusion a
22 Ordering
24 String
32 Int
55 b
102 a
126 PartialOrdering
130 Type
259 'Many
total (230, 1296)
--
3 PartialOrd a
4 LeftClosedPOMonoid a
5 POMonoid a
6 TyCon
8 Addr#
8 TrName
12 Type
13 'Many
15 KindRep
20 a
total (21, 111)
--
12 KindRep
13 Char
15 LiftedRep
24 Integer
31 m
44 b
110 Ptr a
127 Type
177 a
223 'Many
total (219, 1184)
--
6 Addr#
6 TrName
8 StarSemiRing a
13 Maybe a
13 SemiRing a
14 ()
16 KindRep
21 Type
28 a
35 'Many
total (35, 196)
--
16 Applicative m
16 Semigroup doc
19 ReaderT s m doc
19 StateT s m doc
26 s
40 Type
45 m
73 doc
75 'Many
81 b
total (96, 585)
--
11 String
12 KindRep
15 LiftedRep
43 b
48 SmallSetElement a
63 Word64
72 SmallSet a
89 Type
128 a
149 'Many
total (119, 808)
--
12 (k, a)
16 [a] -> [a]
18 k
23 el
29 [a]
29 KindRep
33 coll
77 'Many
149 a
151 Type
total (176, 859)
--
10 Fail
10 (a, NonEmpty c)
11 EquivT s c c Fail
14 a
16 NonEmpty a
18 NonEmpty (NonEmpty a)
22 Type
27 LiftedRep
31 'Many
44 c
total (67, 321)
--
4 CallStack
5 KindRep
6 Addr#
6 TrName
8 String
23 Suffix
24 LiftedRep
25 'Many
26 Integer
39 Char
total (27, 200)
--
15 KindRep
27 Int
31 'Lifted
38 b
38 c
39 Either3 a b c
45 a
101 Three
120 Type
187 'Many
total (180, 1032)
--
25 Maybe v
30 Ord k
35 b
35 Trie k a
77 Trie k v
92 a
97 v
133 k
227 Type
285 'Many
total (292, 1607)
--
12 Pair b
14 Type -> Type
16 d
23 c
36 m
50 Pair a
68 b
109 a
180 Type
223 'Many
total (267, 1153)
[ 50 of 427] Compiling Agda.Utils.List1[boot] ( src/full/Agda/Utils/List1.hs-boot, interpreted )
1 Type -> Type
1 NonEmpty
1 Module
1 'Many
2 Type
total (5, 6)
--
20 Eq a
23 [b]
24 Bool
48 LiftedRep
49 b
89 Int
185 Type
233 [a]
274 a
383 'Many
total (382, 2152)
--
12 Bool
20 LiftedRep
26 m
26 NonEmpty a
46 [a]
47 List1 a
48 b
105 Type
114 a
171 'Many
total (222, 997)
--
8 String -> String
8 Monad m
8 IsString (m a)
10 Type -> Type
12 a
17 [Char]
25 String
26 Type
39 'Many
44 Char
total (63, 290)
--
10 Peano -> Peano
10 Sized a
12 k
14 SizedThing a
17 Int
19 KindRep
39 Peano
72 'Many
76 a
102 Type
total (131, 586)
--
34 m
35 KindRep
48 [Int]
52 LiftedRep
82 Drop a
86 Permutation
129 a
201 Type
207 Int
380 'Many
total (386, 2231)
--
31 'Lifted
34 [Char]
36 C
38 ProfileOptions
42 String
45 U1 @Type
67 x
114 Type
134 'Many
169 ProfileOption
total (169, 1301)
--
12 Int
16 Ord a
17 String
22 [a]
26 m
43 b
105 List2 a
138 Type
170 a
241 'Many
total (230, 1211)
--
6 Word64
6 CallStack
7 Maybe Word64
7 (Integer, Integer)
9 LiftedRep
18 Int
19 Double -> Double
47 'Many
53 Integer
117 Double
total (51, 369)
--
10 (Either (List1 a) (List1 b), [Either a b])
11 c1
11 [Either a b]
12 d
13 m
17 Either a b
48 b
60 a
84 Type
92 'Many
total (158, 614)
--
35 m Bool
36 e
38 [a]
41 b
54 Monad m
74 a
92 Type -> Type
103 Type
134 m
261 'Many
total (294, 1495)
--
53 Applicative m
65 LiftedRep
74 Monad m
78 b
100 ListT m a
117 Type -> Type
138 a
148 Type
211 m
378 'Many
total (370, 2198)
--
6 Text -> Text -> Bool
8 Int
8 LiftedRep
14 String
15 IO
22 Bool
31 Text
34 FilePath
41 AbsolutePath
72 'Many
total (58, 327)
--
2 AbsolutePath
3 Word8
4 String
4 Word64
4 LiftedRep
4 ByteString
4 Text
9 'Many
9 Hash
10 Hash
total (28, 74)
--
35 Map k v
41 HasTag v
47 Ord k
51 Maybe v
54 Tag v
107 BiMap k v
169 k
202 v
257 Type
392 'Many
total (404, 2259)
--
16 Int
17 x
18 KindRep
24 Word64
34 String
47 range
53 ModuleNameHash
63 TopLevelModuleName' range
101 Type
107 'Many
total (159, 763)
--
120 D
122 Addr#
122 TrName
144 'Many
331 WarningName
351 Zero
462 C
570 U1 @Type
1254 x
1755 Type
total (873, 9775)
--
9 Any @Type
11 U1 @Type
12 String
12 Zero
14 C
17 x
30 Help
40 HelpTopic
48 'Many
50 Type
total (105, 452)
--
16 CompareResult a
18 LiftedRep
19 []
20 PartialOrd a
32 [a]
61 b
69 Favorites a
142 a
153 Type
194 'Many
total (175, 1058)
--
8 f
8 LiftedRep
8 AssocList k v
9 m
9 [(k, v)]
21 (k, v)
26 v
29 k
47 Type
69 'Many
total (100, 377)
--
26 Proxy @{Type} b
35 [Type]
42 as
43 l
46 KindRep
49 a
65 k
68 b
139 'Many
225 Type
total (215, 1264)
[ 71 of 427] Compiling Agda.Syntax.Position[boot] ( src/full/Agda/Syntax/Position.hs-boot, interpreted )
1 Type
1 TyCon
1 Module
total (3, 3)
--
74 m
93 String
93 Range
101 Interval' a
135 Range' a
151 Position' a
199 b
534 a
939 Type
1200 'Many
total (1311, 7290)
--
53 NameKind
62 KindRep
81 b
110 OtherAspect
116 String
120 C
144 U1 @Type
251 'Many
358 x
612 Type
total (562, 3949)
--
21 String
22 KindRep
32 LiftedRep
75 Int
86 Pretty a
98 a
121 Aspects
134 Type
262 Doc
278 'Many
total (352, 1954)
--
6 Type
7 Bool
8 LiftedRep
9 Integer -> Integer -> Integer
9 Integer -> Integer
9 Int
13 m
39 CPUTime
64 Integer
97 'Many
total (76, 386)
--
53 Docs k
63 b
67 LiftedRep
90 KindRep
115 a
211 tok1
226 r
246 k
373 'Many
578 Type
total (543, 3493)
--
80 Map n e
102 Edge n e
109 Int
116 LiftedRep
122 Ord n
146 Graph n e
338 e
523 Type
525 n
863 'Many
total (814, 5246)
--
5 [a]
6 Map n (Maybe ())
8 LiftedRep
8 (n, Map n (Maybe ()))
9 a
9 [n]
15 [(n, Map n (Maybe ()))]
16 Maybe ()
28 n
30 'Many
total (44, 192)
--
3 Type
4 Int
4 [Char]
4 DotGraph
7 WithUniqueInt Text
7 ()
8 [Text]
10 LiftedRep
16 'Many
36 Text
total (37, 141)
--
3 SrcLoc -> Doc
3 CallSite -> Doc
5 CallSite
6 []
6 CallStack
8 Int
8 SrcLoc
10 Aspects
12 'Many
37 Doc
total (31, 126)
[ 81 of 427] Compiling Agda.Utils.CallStack ( src/full/Agda/Utils/CallStack.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
--
37 x
49 CPUTime
56 a
56 r
86 LiftedRep
97 MonadBench m
104 Type -> Type
259 Type
273 m
313 'Many
total (524, 2871)
--
55 Size i
57 String
71 MIx i
73 Ord i
87 Matrix i b
135 a
136 b
300 i
423 Type
663 'Many
total (607, 3500)
--
15 String
18 Type
19 IP "cutoff" CutOff
22 KindRep
29 LiftedRep
29 Matrix Int Order
34 Bool
82 Int
121 Order
139 'Many
total (125, 797)
--
35 Matrix ArgumentIndex a
38 CMSet cinfo
42 String
44 KindRep
55 Int
79 CallMatrixAug cinfo
92 cinfo
134 a
283 Type
348 'Many
total (348, 1998)
--
26 KindRep
27 Graph Node (CMSet cinfo)
29 LiftedRep
32 Node
34 CMSet cinfo
56 b
84 CallGraph cinfo
96 cinfo
105 Type
165 'Many
total (213, 1105)
--
7 Node
8 IP "cutoff" CutOff
8 Either cinfo ()
9 [Call cinfo]
12 Type
14 [CallMatrixAug cinfo]
14 CallMatrixAug cinfo
20 LiftedRep
24 cinfo
31 'Many
total (47, 214)
--
12 Bool
13 SpecialCharacters
15 'Lifted
18 KindRep
22 Int
23 Aspects
32 Type
52 Doc
96 'Many
109 UnicodeOrAscii
total (108, 658)
--
7 Ord (Maybe RangeFile)
7 Ord (Range' (Maybe RangeFile))
8 Bool
11 String
12 KindRep
12 RangeFile
16 Maybe RangeFile
31 Range
40 KwRange
54 'Many
total (59, 289)
--
8 Pretty a
9 Char
9 Doc
12 KindRep
16 Lisp String
19 String
19 Type
21 Lisp a
22 a
37 'Many
total (56, 283)
--
349 'Lifted
406 LiftedRep
412 x
484 KindRep
493 Int
610 String
1139 a
1219 b
3557 Type
5922 'Many
total (5271, 36594)
--
24 [(LayerRole, String)]
26 Layer
27 [Char]
32 LayerRole
34 Regex
38 LiftedRep
44 (LayerRole, String)
45 Char
97 String
118 'Many
total (113, 836)
--
44 Zero
45 U1 @Type
45 Precedence
48 ThingWithFixity a
51 C
63 a
71 ParenPreference
110 x
234 'Many
269 Type
total (352, 2018)
--
15 U1 @Type
19 PrecedenceKey
20 MaybePlaceholder tok
21 tok
21 C
32 Zero
35 'Many
45 x
48 MemoKey
113 Type
total (155, 772)
--
48 NameParts
54 LiftedRep
54 KindRep
78 Type
82 NameInScope
84 String
105 NamePart
107 QName
156 Name
346 'Many
total (305, 2045)
--
39 TrName
40 GlobalId
42 Int
53 Comment
54 Exp
64 MemberId
106 KindRep
120 Type
221 String
329 'Many
total (308, 2108)
--
3 LocalId
3 ([MemberId], Exp)
5 Nat -> LocalId -> Exp
6 Exp -> Exp
9 [Exp]
9 (Comment, Exp)
14 MemberId
34 Nat
64 'Many
64 Exp
total (34, 247)
--
36 String
41 Int
41 KindRep
43 a
49 b
51 LiftedRep
55 Char
81 Type
221 'Many
256 Doc
total (247, 1594)
--
325 TyCon
327 Addr#
327 TrName
327 D
380 BuiltinId
965 Zero
1282 C
1590 U1 @Type
3652 x
4966 Type
total (2118, 25088)
--
72 Name
75 KindRep
90 a
91 LiftedRep
113 ModuleName
128 String
153 Type
162 QName
207 Name
546 'Many
total (531, 3383)
--
43 Int
46 String
51 Zero
59 C
60 OccursWhere
76 Where
124 x
169 Occurrence
188 'Many
236 Type
total (308, 2309)
--
'MetaSel
('Nothing @Symbol)
'NoSourceUnpackedness
'NoSourceStrictness
'DecidedLazy
15 RecordFieldWarning
20 String
26 x
28 KindRep
55 Type
total (85, 366)
--
11 Int
15 LiftedRep
16 Char
16 'One
16 Doc
17 QName
36 KindRep
45 String
56 'Many
64 Literal
total (85, 500)
--
96 R
123 S
175 U1 @Type
207 String
209 Zero
215 TTerm
231 C
451 'Many
507 x
914 Type
total (837, 6836)
--
2 Addr#
2 TrName
2 ([TAlt], [TAlt])
3 TTerm -> TTerm
3 []
4 CallStack
5 [TAlt]
9 TTerm
10 'Many
14 TAlt
total (17, 62)
--
10 TAlt
13 KindRep
17 String
20 LiftedRep
26 AsPat
27 [AsPat]
33 Int
38 ReaderT [AsPat] Identity
64 'Many
70 TTerm
total (75, 457)
--
22 Token
23 Interval
23 Symbol
37 Keyword
38 KindRep
47 'Many
50 String
113 TyCon
115 Addr#
115 TrName
total (74, 790)
--
412 KillRange
448 Bool
608 [Type]
623 KindRep
628 a
705 Expr
762 '[] @Type
1013 LiftedRep
1853 Type
2123 'Many
total (2752, 23277)
--
12 LiftedRep
18 KindRep
18 Range
23 TopLevelModuleName
26 Text
29 String
30 TopLevelModuleNameParts
34 Type
94 'Many
97 RawTopLevelModuleName
total (159, 707)
--
136 []
156 Doc Aspects
171 a
250 LiftedRep
265 Type
272 Int
370 Aspects
788 'Many
885 Doc
1813 String
total (1001, 8348)
--
34 Zero
47 KindRep
53 String
56 a
59 x
60 SplitTree' a
67 LazySplit
84 SplitTag
180 'Many
234 Type
total (344, 1972)
--
46 NotationKind
47 Zero
52 KindRep
57 Int
64 LiftedRep
80 NewNotation
83 x
99 String
188 Type
207 'Many
total (385, 2417)
--
13 Int
25 Arg a
27 m
29 String
31 KindRep
49 b
71 Elim' a
130 a
132 Type
206 'Many
total (247, 1207)
--
64 LiftedRep
68 String
94 Blocked' t a
103 x
127 b
135 a
164 t
193 Blocker
428 'Many
553 Type
total (643, 3937)
--
279 b
279 '[] @Type
381 KindRep
385 x
390 Term
553 LiftedRep
726 String
858 a
2487 'Many
2671 Type
total (3360, 23910)
--
6 PlusLevel
9 Maybe Int
10 Term
17 String
17 DeBruijn a
18 Type
19 Int
21 a
22 KindRep
54 'Many
total (61, 286)
--
22 Sort
23 Sort' Term
37 Identity
38 PrecomputeFreeVars a
54 IntSet
59 Type
62 WriterT IntSet Identity
65 Term
74 a
136 'Many
total (186, 974)
--
68 KindRep
70 IgnoreSorts
87 VarOcc' a
116 FlexRig' a
146 LiftedRep
199 b
226 c
493 a
653 Type
816 'Many
total (896, 5650)
--
24 Term
31 Type
38 'One
39 TyCon
41 Addr#
41 TrName
45 Int
87 'Many
105 KindRep
191 String
total (122, 950)
--
43 Pattern' a
45 KindRep
47 DeBruijnPattern
80 b
93 Int
104 LiftedRep
105 m
119 a
326 Type
411 'Many
total (557, 3104)
--
52 Monad m
58 Type -> Type
82 TermLike a
84 Term -> m
85 Term -> m Term
103 a
116 Term
182 Type
392 m
473 'Many
total (505, 2800)
--
73 KindRep
76 CompiledClauses' a
85 x
92 c
109 String
116 m
187 b
301 a
664 Type
718 'Many
total (935, 5486)
--
14 Term
16 AllMetas b
20 MetaId
29 MetaId -> m
34 a
34 AllMetas a
35 Monoid m
78 m
132 Type
191 'Many
total (225, 943)
--
31 KindRep
34 GetDefs a
36 Monad m
38 b
39 MonadGetDefs m
44 Type -> Type
70 ()
73 Type
128 m
144 'Many
total (214, 1117)
--
52 KindRep
61 Type -> Type
63 Pattern -> m Pattern
74 LiftedRep
83 CPatternLike p
144 p
184 Type
200 Pattern
263 m
518 'Many
total (499, 3026)
--
26 MemoKey
26 Expr
30 Int
36 Pattern
52 MaybePlaceholder e
56 LiftedRep
81 Type
105 KindRep
129 e
251 'Many
total (368, 1963)
--
97 Type -> Type
146 Declaration
158 ExprLike a
159 Expr -> Expr
164 LiftedRep
191 Expr
249 a
384 m
420 Type
918 'Many
total (970, 5568)
--
29 Fixity'
40 KindRep
41 Type -> Type
43 MonadicFixPol m
58 DeclaredNames
68 LiftedRep
89 b
94 Name
111 m
182 'Many
total (184, 1381)
--
425 S
464
'MetaSel
('Nothing @Symbol)
'NoSourceUnpackedness
'NoSourceStrictness
'DecidedLazy
901 String
921 x
1443 Type
total (905, 9698)
--
'NoSourceStrictness
'DecidedLazy
116 Zero
118 S
130 LiftedRep
150 Doc
221 C
277 String
473 x
841 Type
total (536, 5729)
--
39 ()
42 LoneSig
43 Nice
45 NiceEnv
48 Name
75 KindRep
105 a
116 NiceState
143 Type
252 'Many
total (274, 1877)
--
15 Cohesion
19 Type
19 Relevance
21 KindRep
22 Quantity
48 LiftedRep
57 a
61 String
68 Attribute
104 'Many
total (113, 761)
--
37 Aspects
42 LiftedRep
64 'One
66 ParseError
80 a
109 ParseState
115 KindRep
143 Type
297 'Many
332 String
total (294, 2358)
--
17 CurrentInput
17 PreviousInput
18 LexAction a
22 b
22 ParseState
25 AlexInput
32 a
35 KindRep
59 Type
154 'Many
total (139, 711)
--
21 KindRep
21 LookAhead b
27 Char
28 StateT AlexInput Parser
30 ErrorFunction
31 b
47 AlexInput
56 a
99 Type
100 'Many
total (124, 784)
--
8 Literal
11 Token
12 ()
13 Int
25 LookAhead
27 String
28 LiftedRep
47 (String, Char)
60 Char
65 'Many
total (66, 420)
[137 of 427] Compiling Agda.Syntax.Parser.Layout[boot] ( src/full/Agda/Syntax/Parser/Layout.hs-boot, interpreted )
1 Module
1 Token
1 Parser ()
1 ()
3 LexAction Token
total (5, 7)
--
2 LexAction r
3 LexState
3 LexPredicate
3 LexAction tok
4 tok
4 String
5 a
7 LexAction Token
10 Type
23 'Many
total (60, 123)
--
6 PreviousInput -> CurrentInput -> TokenLength -> Parser Token
9 Type
9 LookAhead ()
9 ()
10 a
10 String
11 Parser
16 Token
22 LiftedRep
36 'Many
total (55, 232)
--
32 AlexInput
38 Int
38 KindRep
58 Type
72 Keyword -> LexAction Token
120 'Many
152 LexAction Token
575 (Int, LexAction Token)
628 AlexAcc ([LexState], ParseFlags)
653 ([LexState], ParseFlags)
total (155, 2817)
--
16 String
18 Parser
22 a
24 Type
25 Interval
28 Integer
39 Token
40 Char
48 LiftedRep
142 'Many
total (130, 766)
--
6 LexAction Token
9 PreviousInput -> CurrentInput -> TokenLength -> Parser Token
10 LayoutStatus
10 Parser ()
13 ()
14 Column
20 LiftedRep
20 Token
27 Parser
39 'Many
total (47, 256)
--
40 Char
41 KindRep
46 CallStack
46 Name
49 String
52 Attr
105 Parser
121 Expr
204 LiftedRep
331 'Many
total (454, 2727)
--
-> Happy_IntList
-> HappyStk HappyAbsSyn
-> Parser HappyAbsSyn
586 Token
606 b
631 LiftedRep
934 KindRep
2202 'Many
2241 Type
3390 HappyAbsSyn
total (1067, 22495)
--
22 b
23 ExceptT ParseError (StateT [ParseWarning] IO)
28 IO
28 StateT [ParseWarning] IO
34 ParseError
46 [ParseWarning]
72 KindRep
73 a
135 Type
152 'Many
total (227, 1263)
--
43 TrName
43
'MetaData "Phase" "Agda.Benchmarking" "Agda-2.6.5-inplace" 'False
62 Phase
67 'Many
123 Zero
162 C
190 U1 @Type
380 x
572 Type
total (369, 3106)
--
34 KindRep
37 a
42 SingleFlexRig
42 SingleVarOcc
42 VarCounts
47 LiftedRep
61 c
90 Type
120 b
280 'Many
total (242, 1547)
--
31 SubstArg a
32 Nat
39 Subst a
43 KindRep
45 LiftedRep
63 Int
72 Substitution' a
97 Type
181 a
207 'Many
total (176, 1246)
--
188 Scope
199 C
220 S
253 KindRep
253 Zero
323 LiftedRep
397 String
482 x
1201 Type
1476 'Many
total (1937, 14236)
--
108 ConPatLazy
116 Zero
121 R
126 Range
128 KindRep
159 S
183 x
321 String
495 'Many
569 Type
total (853, 5330)
--
'NoSourceUnpackedness
'NoSourceStrictness
'DecidedLazy
767 R
892 S
973 LiftedRep
1542 String
1829 x
2103 'Many
4693 Type
total (4589, 40252)
--
76 Expr -> Expr
78 Declaration
118 Expr -> m Expr -> m Expr
149 Type -> Type
170 ExprLike a
278 a
528 Type
682 Expr
1024 m
1257 'Many
total (1146, 7922)
--
17 KindRep
24 e
32 a
36 BoundAndUsed a
37 Set Name
42 Expr
56 b
118 Type
155 BoundAndUsedNames
212 'Many
total (323, 1407)
--
16 Pattern' e1
16 Expr
20 f
24 Maybe
25 e
28 ()
29 Pattern' e
31 Type
31 Name
68 'Many
total (153, 635)
--
38 NamedArg (Pattern' e)
40 Pattern' e
61 Pattern' a
68 e
71 KindRep
122 LiftedRep
144 a
199 m
242 Type
530 'Many
total (597, 3385)
--
67 Aspects
70 FilePath
74 LiftedRep
90 S
103 x
104 KindRep
131 Doc
194 String
307 Type
307 'Many
total (552, 3740)
--
26 [String]
28 AgdaLibFile
30 [Char]
33 LibParseError
34 LiftedRep
39 ExceptT LibParseError (Writer [LibWarning'])
40 Char
60 KindRep
88 String
143 'Many
total (183, 1079)
--
8 Int32
9 ()
10 LiftedRep
13 KindRep
19 [Range]
25 String
25 Ranges
37 Int
78 Range
85 'Many
total (72, 422)
--
43 b
53 KindRep
61 PairInt a
63 LiftedRep
78 Map Int (PairInt a)
98 RangeMap a
108 Type
126 Int
198 'Many
221 a
total (197, 1544)
--
42 hl
42 Key
54 C
75 U1 @Type
93 PositionMap
98 Zero
98 Aspects
168 b
178 Type
313 'Many
total (502, 2589)
--
4 [KindRep]
5 TyCon
6 b
6 'False
6 'True
7 Addr#
7 TrName
8 'Many
10 Bool
23 KindRep
total (27, 106)
--
1 a -> Bool
1 forall a. a -> a -> Bool
1 Bool
1 Module
2 Addr#
2 Type
2 TrName
2 'Lifted
4 'Many
6 a
total (11, 23)
--
44 (a, Bool)
61 Any
62 b
74 LiftedRep
76 Identity
115 Type -> Type
147 m
179 a
212 Type
299 'Many
total (347, 2181)
--
101 ChangeT Nice
110 ([NiceDeclaration], [Declaration])
115 Declaration
136 CallStack
148 Name
185 [NiceDeclaration]
293 NiceDeclaration
323 LiftedRep
370 Nice
678 'Many
total (494, 5347)
--
1 VarSet -> VarSet
1 Type
1 Module
1 Key
1 IntSet
2 Addr#
2 Int
2 TrName
2 VarSet
3 'Many
total (11, 17)
--
34 Graph
42 NodeId
44 Rigid
62 Node
71 KindRep
71 Weight
74 Doc
76 Type
127 Int
289 'Many
total (259, 1774)
--
7 Eq a
8 Show a
10 Boolean a
12 KindRep
27 b
39 WithDefault' a b
41 Bool
41 Type
49 a
70 'Many
total (95, 429)
--
17 [a]
18 KindRep
22 g
26 m
32 f
40 b
87 ListZipper a
154 a
166 Type
274 'Many
total (289, 1461)
--
2 (# #)
3 IO a
4 Int
5 String
7 IO FilePath
8 IO
8 IOException
10 Char
20 'Many
27 FilePath
total (28, 117)
--
5 LiftedRep
5 'MetaData
"AnArbitrarySymbolInThisPackage"
"Agda.Version"
"Agda-2.6.5-inplace"
'False
6 'Many
8 String
8 AnArbitrarySymbolInThisPackage
12 Type
total (37, 109)
--
2 Addr#
2 [a]
2 Maybe String
2 Type
2 LiftedRep
2 TrName
4 'Many
6 String
7 Char
9 [Char]
total (16, 45)
--
38 StateT LibState IO
39 AgdaLibFile
40 [FilePath]
48 String
49 IO
53 [AgdaLibFile]
97 WriterT LibErrWarns (StateT LibState IO)
128 FilePath
135 LiftedRep
177 'Many
total (319, 2059)
--
261 LiftedRep
261 Zero
323 WithDefault 'False
487 S
546 x
582 Bool
683 PragmaOptions
1155 'Many
1299 Type
1305 String
total (1599, 15147)
--
15 n
15 w
17 Monad m
21 PragmaOptions
21 CommandLineOptions
54 Type
107 HasOptions m
121 Type -> Type
139 'Many
178 m
total (236, 1062)
--
3 Doc
4 Bool
4 Type
5 Aspects
5 Aspect
7 ()
9 IO ()
10 m
17 'Many
33 SGR
total (36, 135)
[176 of 427] Compiling Agda.Interaction.Options ( src/full/Agda/Interaction/Options.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
[177 of 427] Compiling Agda.Compiler.Treeless.Pretty[boot] ( src/full/Agda/Compiler/Treeless/Pretty.hs-boot, interpreted )
1 Module
1 Pretty Compiled
1 Compiled
total (3, 3)
--
2 a
2 IORef TCState -> TCEnv -> m a
2 HighlightingLevel
2 HighlightingMethod
4 TCMT m
7 m
8 Type -> Type
8 'Many
14 TyCon
21 Type
total (47, 107)
--
23 opts
28 [KindRep]
36 R
36 S
37 Backend'_boot tcm opts env menv mod def
46 Type -> Type
62 x
67 'Many
127 KindRep
360 Type
total (336, 1513)
--
179 'One
183 ReadPrec
185 range
220 KindRep
253 Interaction' range
272 b
344 a
455 Type
760 String
824 'Many
total (747, 6826)
--
10 ResponseContextEntry
11 Expr
13 'Many
54 [KindRep]
63 Addr#
63 TrName
64 TyCon
72 'One
124 Type
253 KindRep
total (74, 846)
--
'DecidedLazy
2244 KindRep
2543 C
2963 R
3203 Zero
3749 S
4320 String
8413 x
9445 'Many
17317 Type
total (16544, 137494)
--
150 Args
157 CallStack
168 Subst a
172 t
223 Sort
564 a
666 Type
770 LiftedRep
883 Term
2463 'Many
total (1735, 13455)
--
32 All
32 Any
33 a
38 KindRep
52 b
56 Type
62 TTerm
72 Int
102 Occurs
237 'Many
total (196, 1206)
--
42 TTerm
50 Aspects
54 Doc Aspects
67 ReaderT PEnv Identity
68 P Doc
74 PEnv
85 Int
105 LiftedRep
123 Doc
144 'Many
total (151, 1305)
--
4 Int
4 [a]
5 (# #) -> Bool
5 TAlt
6 Bool
6 (# #)
7 a
15 TTerm
30 'Many
37 Integer
total (35, 153)
--
2 (# #)
3 m
3 TTerm -> TTerm
4 Int
4 CallStack
8 LiftedRep
9 TPrim
13 TAlt
36 'Many
51 TTerm
total (39, 173)
--
66 Dict
69 'One
96 IO
111 LiftedRep
123 t
141 a
190 KindRep
233 Int32
293 Type
415 'Many
total (407, 3611)
--
10 TCState
11 TCMT IO ()
13 Map TopLevelModuleName ModuleInfo
14 ModuleInfo
20 m
21 Doc
23 TCMT IO
36 TopLevelModuleName
40 LiftedRep
48 'Many
total (88, 418)
--
14 TCEnv -> TCEnv
18 m a -> m a
18 TCEnv
22 a
26 Type -> Type
26 MonadTCEnv m
30 Type
32 m
36 LiftedRep
70 'Many
total (91, 480)
--
2 SomeBuiltin -> m (Maybe (Builtin PrimFun))
2 forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type).
(MonadTrans t, HasBuiltins n, (~) @(Type -> Type) (t n) m) =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
2 TyCon
4 HasBuiltins m
5 Type
10 Type -> Type
11 m
11 'Many
total (51, 92)
--
forall (m :: Type -> Type).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
223 MonadError TCErr m
223 ReadTCState m
225 MonadTCEnv m
360 HasBuiltins m
383 Type -> Type
624 m
1365 'Many
total (585, 6252)
--
2 TCMT IO Defn
3 []
3 (# #)
5 IO
7 LiftedRep
8 TCMT IO
10 Bool
11 Int
11 Defn
29 'Many
total (55, 144)
--
7 SplitTree' SplitTag
7 Clause
8 a
8 CallStack
8 CompiledClauses
11 KindRep
12 Term
18 LiftedRep
38 Int
45 'Many
total (78, 298)
--
56 Term
59 Semigroup m
81 QName
97 a
118 NamesIn a
128 Monoid m
216 Either QName MetaId -> m
399 Type
639 m
733 'Many
total (830, 4215)
[196 of 427] Compiling Agda.Interaction.Output ( src/full/Agda/Interaction/Output.hs, interpreted )
1 Module
1 OutputConstraint_boot TCErr a b
1 OutputForm_boot TCErr a b
2 a
2 b
2 Addr#
2 TrName
2 TCErr
6 Type
total (9, 19)
--
1 Args
1 ReduceM (Reduced (Blocked [Elim]) Term)
1 ReduceM (Reduced (Blocked Args) Term)
1 MaybeReducedElims
1 MaybeReducedArgs
1 Reduced (Blocked [Elim]) Term
1 Reduced (Blocked Args) Term
2 Term
2 CompiledClauses
4 'Many
total (19, 24)
[198 of 427] Compiling Agda.TypeChecking.Reduce.Fast[boot] ( src/full/Agda/TypeChecking/Reduce/Fast.hs-boot, interpreted )
1 Term -> ReduceM (Blocked Term)
1 Term -> ReduceM Term
1 Module
1 Blocked Term
1 ReduceM (Blocked Term)
1 ReduceM Term
2 'Many
4 Term
total (8, 12)
--
1 TopLevelModuleName
-> ModuleName -> TCM (ModuleName, Map ModuleName Scope)
1 Module
1 Map ModuleName Scope
1 TopLevelModuleName
1 Scope
1 TCM (ModuleName, Map ModuleName Scope)
1 (ModuleName, Map ModuleName Scope)
2 'Many
3 ModuleName
total (10, 13)
--
1 Type
1 Module
1 QName
1 BackendName
1 TCM
1 TCM Bool
1 TCM (Maybe Backend)
1 Backend_boot TCM
1 Backend
2 'Many
total (14, 15)
[201 of 427] Compiling Agda.Compiler.Builtin[boot] ( src/full/Agda/Compiler/Builtin.hs-boot, interpreted )
1 [Backend]
1 Module
1 Backend
total (3, 3)
[202 of 427] Compiling Agda.Compiler.Treeless.Erase[boot] ( src/full/Agda/Compiler/Treeless/Erase.hs-boot, interpreted )
1 QName -> TCM Bool
1 Bool
1 Module
1 'Many
1 QName
1 TCM Bool
total (6, 6)
--
1 Type -> Arg Term -> Type -> TCM ()
1 Type -> TCM ()
1 Term -> Type -> Arg Term -> Type -> TCM ()
1 Module
1 Arg Term
1 TCM ()
1 ()
2 Type
2 Term
4 'Many
total (11, 16)
--
2 Range
2 Telescope
3 Term
3 Args
3 ExpandHidden
4 Comparison
4 TCM Term
6 Type
6 Expr
34 'Many
total (64, 122)
--
1 Module
1 QName
1 SplitTree
1 Clause
1 Type
1 CompiledClauses
1 TCM (Maybe SplitTree, Bool, CompiledClauses)
1 (Maybe SplitTree, Bool, CompiledClauses)
1 (QName, Type)
2 'Many
total (16, 17)
[206 of 427] Compiling Agda.TypeChecking.Rules.Data[boot] ( src/full/Agda/TypeChecking/Rules/Data.hs-boot, interpreted )
1 QName -> Sort -> TCM ()
1 Sort -> TCM ()
1 Module
1 QName
1 Sort
1 TCM ()
1 ()
2 'Many
total (8, 9)
--
1 ModuleApplication
1 ImportDirective
1 DefInfo
1 ScopeCopyInfo
1 Expr
1 ()
2 Erased
2 Declaration
4 TCM ()
14 'Many
total (31, 49)
[208 of 427] Compiling Agda.Interaction.Highlighting.Generate[boot] ( src/full/Agda/Interaction/Highlighting/Generate.hs-boot, interpreted )
1 TCWarning -> TCM ()
1 Module
1 'Many
1 TCM ()
1 TCWarning
1 ()
total (6, 6)
--
1 ()
1 (List1 (WithHiding Name), Maybe Type)
1 (Term, Type)
2 Type -> TCM Term
3 Expr -> Type -> TCM Term
3 Expr
3 Comparison
5 Type
5 Term
12 'Many
total (30, 56)
[210 of 427] Compiling Agda.TypeChecking.Primitive[boot] ( src/full/Agda/TypeChecking/Primitive.hs-boot, interpreted )
1 Module
1 Map PrimitiveId (TCM PrimitiveImpl)
1 PrimitiveId
1 TCM PrimitiveImpl
1 PrimitiveImpl
total (5, 5)
--
1 [AbsolutePath]
1 Module
1 AbsolutePath
1 LibM a
1 HasOptions m
1 TCM a
2 a
2 m
3 Type
3 'Many
total (16, 22)
--
1 Level -> m Term
1 HasBuiltins m => Level -> m Term
1 forall (m :: Type -> Type). HasBuiltins m => Level -> m Term
1 Module
1 Level
1 Term
1 HasBuiltins m
2 m
2 Type
3 'Many
total (12, 16)
--
2 MonadTrans t
2 InteractionId
2 InteractionPoints
2 ReadTCState m
2 MonadInteractionPoints n
5 Type
5 MonadInteractionPoints m
10 m
12 Type -> Type
17 'Many
total (61, 119)
--
4 m a
4 (Type -> Type) -> Type -> Type
4 (~) @(Type -> Type) (t n) m
4 MonadTransControl t
4 MonadAddContext n
7 m
7 MonadAddContext m
13 Type
16 Type -> Type
36 'Many
total (99, 206)
[215 of 427] Compiling Agda.TypeChecking.Monad.Debug[boot] ( src/full/Agda/TypeChecking/Monad/Debug.hs-boot, interpreted )
1 Type -> Type
1 TyCon
1 Module
1 'Many
2 Type
total (5, 6)
--
1 MonadTCM tcm
1 MonadTCEnv m
1 ReadTCState m
1 MonadDebug m
2 tcm
2 Type -> Type
2 Type
2 QName
4 m
7 'Many
total (23, 36)
--
87 a
104 VerboseKey
108 LiftedRep
122 VerboseLevel
124 String
187 Type
264 MonadDebug m
312 Type -> Type
491 m
732 'Many
total (764, 4397)
--
17 Integer -> Integer
19 ()
20 KindRep
23 Integer
28 Type
35 String
40 MonadStatistics m
53 Type -> Type
70 m
120 'Many
total (176, 781)
--
4 MonadTCM tcm
5 tcm
6 ()
7 'Many
8 IO
9 Phase
9 TCMT IO (BenchmarkOn Phase)
16 BenchmarkOn Phase
20 LiftedRep
23 TCMT IO
total (32, 144)
--
17 m1
18 Maybe LoadedFileCache
18 LoadedFileCache
19 MonadTCState m
22 m ()
25 ()
26 Type -> Type
40 LiftedRep
70 m
97 'Many
total (113, 618)
--
2 TCM a
2 Definition
2 HasConstInfo n
4 QName
5 HasConstInfo m
6 Type
6 TyCon
12 Type -> Type
15 m
21 'Many
total (76, 153)
--
1 forall (m :: Type -> Type). HasConstInfo m => QName -> m Bool
1 Bool
1 Module
1 TCM ()
1 HasConstInfo m
1 ()
2 m
2 Type
2 QName
4 'Many
total (15, 21)
--
1 TCState
1 TCEnv
1 Definition
1 MonadTCEnv m
1 ReadTCState m
1 HasConstInfo m
2 Bool
2 Type
4 m
8 'Many
total (22, 34)
--
1 PureTCM (StateT s m)
1 PureTCM (WriterT w m)
1 PureTCM TCM
2 w
2 TyCon
4 PureTCM m
5 Type -> Type
6 Type
6 'Many
12 m
total (40, 70)
--
4 forall (m :: Type -> Type) (t :: Type -> Type).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
5 a
7 Applicative m
7 Type
9 m
12 m Doc
12 Type -> Type
23 'Many
total (95, 179)
--
1 Module
1 Range
1 Doc
1 Call
1 Closure Call
1 MonadPretty m
2 m
2 m Doc
2 Type
5 'Many
total (17, 24)
--
1 Module
1 WarningName
1 Doc
1 Warning
2 m
2 m Doc
2 Type -> Type
2 Type
2 MonadPretty m
5 'Many
total (16, 25)
--
28 HasOptions m
28 Warning
28 MonadInteractionPoints m
30 MonadFresh NameId m
32 TCWarning
36 MonadWarning m
37 WhichWarnings
53 Type -> Type
117 m
149 'Many
total (247, 1336)
--
1 Goals_boot TCErr
1 GoalDisplayInfo_boot TCErr
1 DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
1 Response_boot TCErr TCWarning WarningsAndNonFatalErrors
2 Addr#
2 TrName
2 WarningsAndNonFatalErrors
3 TCWarning
5 Type
5 TCErr
total (12, 25)
--
37 Signature
40 Type -> Type
52 ScopeInfo
55 ()
60 a
60 QName
77 m
138 LiftedRep
139 TCMT IO
428 'Many
total (345, 2391)
--
32 Closure Call
36 TCEnv
69 Call
83 a
103 MonadTrace m
106 LiftedRep
116 Type -> Type
155 Type
208 m
370 'Many
total (426, 2453)
--
11 Substitution
12 Type -> Type
12 LiftedRep
14 MaybeT m
14 Open a
20 CheckpointId
21 Type
29 a
36 m
61 'Many
total (108, 434)
--
76 MonadTCEnv m
146 Term
180 Name
180 MonadAddContext m
219 a
240 LiftedRep
264 Type -> Type
309 Type
473 m
950 'Many
total (1054, 6306)
--
1 HasBuiltins m
1 MonadAddContext m
1 MonadDebug m
1 HasConstInfo m
1 MonadPretty m
1 ()
2 Type
3 Polarity
11 m
14 'Many
total (34, 60)
--
20 MonadTCEnv tcm
23 tcm a
27 TCEnv
28 Type -> Type
30 LiftedRep
35 m
43 a
45 tcm
46 Type
87 'Many
total (135, 743)
--
6 ReadTCState m
8 m b
8 Closure a
9 a
9 b
11 m (Closure b)
14 LiftedRep
16 Type
21 m
30 'Many
total (48, 210)
--
36 Bool
36 ()
39 ProblemConstraint
41 Type
44 LiftedRep
44 KindRep
63 MonadConstraint m
81 Type -> Type
188 m
210 'Many
total (225, 1532)
--
2 m a
2 a -> TCM b
2 TCM b
3 a
3 ProblemId
4 TCM a
4 TCM ()
5 m
6 Type
17 'Many
total (42, 80)
--
86 m
91 ()
93 QName
99 AbstractName
110 Type
137 ModuleName
185 Name
205 TCMT IO
376 LiftedRep
595 'Many
total (730, 5004)
--
13 List1 AbstractName
14 Name
14 AbstractName
15 KindRep
19 Scope
21 Map QName (List1 AbstractName)
24 NewNotation
36 LiftedRep
39 QName
58 'Many
total (118, 535)
--
34 HasBuiltins m
38 QName
44 Type
48 KindRep
54 String
57 DeepSizeView
63 LiftedRep
111 m
119 Term
275 'Many
total (286, 1842)
--
38 PersistentVerbosity
40 SafeMode
44 LiftedRep
50 PragmaOptions
58 CommandLineOptions
72 a
74 Type
75 FilePath
86 KindRep
270 'Many
total (223, 1620)
--
8 Set QName
9 IO
10 tcm
11 Maybe MutualBlock
11 QName
22 LiftedRep
27 TCMT IO
33 MutualId
34 MutualBlock
41 'Many
total (61, 309)
--
54 MemoKey
56 TCMT IO
60 []
63 QName
87 MaybePlaceholder e
94 KindRep
148 Pattern
183 LiftedRep
189 e
319 'Many
total (398, 3118)
--
19 Bool
19 FilePath
23 TopLevelModuleName
30 IO
43 String
56 LiftedRep
60 SourceFile
63 TCMT IO
82 AbsolutePath
138 'Many
total (164, 991)
--
29 PragmaOptions
30 [AbsolutePath]
31 Type -> Type
40 AbsolutePath
41 TopLevelModuleName
60 ()
66 m
108 LiftedRep
111 TCMT IO
145 'Many
total (205, 1367)
--
530 ReaderT Dict IO
608 ReaderT Dict IO Int32
635 EmbPrj
716 a
1470 Int32
1673 'Many
2533 LiftedRep
2615 [Type]
3004 '[] @Type
5357 Type
total (2403, 41079)
--
141 EmbPrj
169 'Many
186 ()
224 Aspect
234 NameKind
245 Int32
282 LiftedRep
477 [Type]
507 '[] @Type
783 Type
total (292, 6059)
--
292 EmbPrj
298 WhyInScope
342 Precedence
460 'Many
470 Pattern' e
489 Int32
1148 LiftedRep
1316 [Type]
1457 '[] @Type
2381 Type
total (811, 17346)
--
1 Blocked Term
1 Type
1 TCM ()
1 ReduceM (Reduced (Blocked Term) Term)
1 Reduced (Blocked Term) Term
1 RewriteRules
1 ()
2 Elims
4 Term
7 'Many
total (19, 29)
--
1 QName -> Elims -> TCM (Reduced () Term)
1 Elims -> TCM (Reduced () Term)
1 Module
1 QName
1 Elims
1 Term
1 TCM (Reduced () Term)
1 Reduced () Term
1 ()
2 'Many
total (10, 11)
--
143 Bool
143 Defn
197 Definition
250 HasConstInfo m
323 Type -> Type
370 QName
400 TCMT IO
537 LiftedRep
645 m
1969 'Many
total (1186, 10469)
--
1 Either SigError ConHead
1 Module
1 ConHead
1 SigError
2 Type -> Type
2 Type
2 HasConstInfo m
3 m
3 QName
5 'Many
total (18, 29)
--
15 e
15 r
15 s
16 w
16 Monoid w
67 Type
151 PureTCM m
152 Type -> Type
168 'Many
206 m
total (295, 1203)
--
Type -> m (Maybe (Term, Term, Term, Term))
1 Maybe (Term, Term, Term, Term)
1 Module
1 Type
1 PureTCM m
1 (Term, Term, Term, Term)
2 m
2 Type
3 'Many
4 Term
total (14, 21)
--
1 Bool
1 Module
1 LensSort a
1 MonadBlock m
1 PureTCM m
1 PrettyTCM a
3 a
3 m
3 Type
6 'Many
total (19, 30)
--
Type -> a -> m Type
2 HasBuiltins m
3 Type -> Type
3 Type
3 MonadReduce m
3 PiApplyM a
4 a
6 m
6 Type
14 'Many
total (42, 79)
--
75 MetaKind
84 CallStack
84 MonadMetaSolver m
95 ReadTCState m
123 Type
129 LiftedRep
155 MetaId
248 Type -> Type
518 m
791 'Many
total (823, 5056)
--
3 String
3 Args
4 Type
4 Type
4 Term
5 m
5 MetaId
8 Type -> Type
8 MonadMetaSolver m
31 'Many
total (80, 154)
[260 of 427] Compiling Agda.TypeChecking.Monad ( src/full/Agda/TypeChecking/Monad.hs, interpreted )
1 Module
2 Addr#
2 TrName
total (3, 5)
--
1 ReadTCState m
1 (QName, Defn)
2 HasConstInfo m => QName -> m Bool
2 Type
2 Defn
5 HasConstInfo m
6 Type -> Type
6 QName
8 m
16 'Many
total (48, 87)
--
2 Args
3 Type -> Term -> Term -> m ()
5 Type
5 Term
6 m ()
6 Comparison
11 m
13 MonadConversion m
14 Type -> Type
43 'Many
total (90, 203)
--
1 DefInfo
1 TCM Definition
1 TCM ()
1 ExtLamInfo
1 ()
2 DefInfo -> QName -> [Clause] -> TCM ()
2 QName
2 TCM a
2 Definition
12 'Many
total (34, 49)
--
3 TypeOf a
3 Type
3 CheckInternal a
3 Action m
6 MonadCheckInternal m
7 a
8 Type
9 Type -> Type
14 m
25 'Many
total (77, 160)
--
2 Args
2 MonadMatch m
2 Match Term
3 a
3 Type -> Type
3 'One
4 m
4 TyCon
8 Type
11 'Many
total (44, 79)
--
1 Module
1 TCM (Either ErrorNonEmpty Int)
1 TCM ()
1 ErrorNonEmpty
1 ()
2 Range
2 Telescope
2 Type
2 TCM Bool
6 'Many
total (21, 30)
[267 of 427] Compiling Agda.TypeChecking.Rules.Builtin.Coinduction[boot] ( src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs-boot, interpreted )
1 Module
1 'Many
1 Type
1 ResolvedName
1 TCM ()
1 ()
3 ResolvedName -> TCM ()
3 TCM Type
total (8, 12)
--
11 String
15 a
15 TCState
17 m
17 ReduceM a
21 Term
28 Type
30 LiftedRep
37 ReduceM
80 'Many
total (146, 549)
--
3 String
3 ReduceM a
4 LiftedRep
4 HasCallStack
5 [String]
6 a
6 Type
8 "callStack"
11 'Many
12 CallStack
total (27, 88)
--
8 HasOptions m
8 MonadTCEnv m
11 Type -> Type
11 KindRep
11 HasConstInfo m
12 m Term
15 LiftedRep
29 m
31 Term
76 'Many
total (90, 379)
--
135 m
172 Constraint
193 Sort
287 t
327 a
336 LiftedRep
742 Type
1078 Term
1079 ReduceM
2220 'Many
total (1963, 14045)
--
82 Type -> Type
82 Telescope
102 a
131 Int
145 Type
167 LiftedRep
174 m
217 Type
221 Term
573 'Many
total (644, 4076)
--
35 FUN 'Many @{LiftedRep} @{LiftedRep}
38 SynEq a
39 Sort
53 ReduceM
69 Type
97 Term
103 Bool
132 a
152 StateT Bool ReduceM
275 'Many
total (338, 2136)
--
39 LevelKit
41 b
53 Level
58 LiftedRep
69 Integer
104 a
107 Type
159 m
163 Term
345 'Many
total (333, 2136)
--
11 t
12 SingleLevel
13 Constraint
18 Int
19 [Leq]
20 LiftedRep
24 SingleLevel' Term
26 Term
28 Leq
52 'Many
total (90, 399)
--
29 a
33 Elim' Term
35 MatchResult
36 Type
42 MaybeT m
49 DisplayTerm
92 m
95 Term
99 LiftedRep
258 'Many
total (273, 1760)
--
32 MonadReader MetaSet m
37 IsFree
38 Reduce a
49 MonadReduce m
49 ForceNotFree a
70 Type
105 Term
116 a
171 m
214 'Many
total (264, 1571)
--
46 Range
47 KindRep
48 QName
52 Expr
68 a
71 Hilite a
130 LiftedRep
192 Type
281 Hiliter
449 'Many
total (609, 3023)
--
14 (Modality, Nat)
15 a
16 [IsForced]
16 ForcedVariables a
18 DList (Modality, Nat)
18 TCMT IO
19 KindRep
20 Modality
28 Type
59 'Many
total (117, 461)
--
11 a
16 KindRep
16 MentionsMeta a
24 t
26 MentionsMeta t
34 Term
38 Bool
46 HashSet MetaId
67 Type
149 'Many
total (192, 757)
--
7 Type
7 ProblemConstraint
8 ()
10 f
13 [MetaId]
16 LiftedRep
18 MetaId
25 Bool
47 'Many
88 m
total (91, 401)
--
13 NamesPerClause
14 CallStack
14 Defn
16 [Clause]
18 Bool
34 TCMT IO
44 LiftedRep
49 Set QName
50 QName
189 'Many
total (133, 812)
--
13 QName
18 b
18 Elim' NLPat
19 m
20 ToNLPat a b
21 a
21 NLPat
28 LiftedRep
68 Type
87 'Many
total (157, 608)
--
51 MonadReflectedToAbstract m
52 ReadTCState m
55 MonadReader Vars m
63 HasOptions m
65 Type -> Type
73 Type
107 Expr
126 LiftedRep
284 m
310 'Many
total (430, 2655)
--
9 []
18 a
20 LiftedRep
23 TTerm
24 ArgUsage
27 Int
30 [ArgUsage]
37 TCMT IO
41 Set Int
49 'Many
total (71, 404)
--
33 String -> ForeignCode
39 'Many
50 [Type]
54 [Char]
57 CompilerPragma
59 '[] @Type
60 ForeignCode
61 SerialisedRange
80 LiftedRep
106 Type
total (105, 1030)
--
1061 FUN 'Many @{LiftedRep} @{LiftedRep}
1139 Term
1280 EmbPrj
1303 ReaderT Dict IO Int32
1913 Int32
2265 'Many
6345 LiftedRep
6566 [Type]
6917 '[] @Type
11644 Type
total (3570, 84833)
--
856 EmbPrj
1027 WithDefault' Bool 'False
1271 'Many
1517 DeclarationWarning'
1558 Int32
2378 Warning
4226 LiftedRep
4633 [Type]
5163 '[] @Type
7837 Type
total (1549, 55102)
--
48 'False
53 EmbPrj
61 [OptionsPragma]
75 ReaderT Dict IO Int32
102 Interface
132 'Many
200 [Type]
205 '[] @Type
333 Type
438 LiftedRep
total (318, 3861)
--
28 String
31 Int32
31 Type
34 a
39 ByteString
44 ()
47 IO
77 TCMT IO
88 LiftedRep
106 'Many
total (238, 1269)
--
17 Bool
20 IO ()
22 Definition
28 LiftedRep
29 IO
30 TCMT IO
36 MetaId
48 ()
63 QName
78 'Many
total (159, 770)
--
9 List1 Expr
10 Type
13 a
15 m
15 QName
15 ()
20 LiftedRep
31 TCMT IO
55 'Many
56 Expr
total (102, 444)
--
11 Name
11 LamClause
13 ScopeM Expr
14 DoStmt
16 Pattern
21 TCMT IO
29 QName
44 LiftedRep
74 'Many
74 Expr
total (91, 477)
--
13 [Char]
16 []
17 List1 String
19 Int
22 Name
26 [String]
28 LiftedRep
29 Char
47 'Many
54 String
total (77, 430)
--
7 (# #)
8 TCMT IO
9 LiftedRep
9 KindRep
9 QName
29 IdentityIn
31 TTerm
41 Int
43 b
71 'Many
total (82, 395)
--
15 Type
18 KindRep
19 BuiltinKit
21 QName
34 LiftedRep
44 QName -> Bool
50 TCMT IO
62 TAlt
102 TTerm
119 'Many
total (110, 776)
--
84 KindRep
85 RWST Env [Output] State m
95 Int
96 State
96 ()
126 String
156 LiftedRep
160 m
185 Text
336 'Many
total (306, 2898)
--
30 ()
35 Attribute
36 Bool
41 HtmlHighlight
48 String
55 Type
55 KindRep
86 LiftedRep
92 Html
159 'Many
total (221, 1462)
--
9 []
9 Args
10 Type -> Type
12 TAlt
14 LiftedRep
14 Nat
18 m
51 'Many
59 m1
107 TTerm
total (57, 389)
--
6 CallStack
6 ExitCode
6 TCMT IO ()
12 Maybe String
15 IO
19 String
22 ()
24 LiftedRep
24 'Many
29 TCMT IO
total (51, 242)
--
19 MaybeReduced Elim
20 [Elim]
21 Reduced (Blocked Elims) Term
25 Elims
26 ReduceM
29 ReduceM (Reduced (Blocked Elims) Term)
39 Elim
74 Term
82 LiftedRep
101 'Many
total (132, 833)
--
4 Defn
6 [QName]
7 QName
8 IO
9 LiftedRep
11 [TAlt]
23 TAlt
42 TCMT IO
43 'Many
57 TTerm
total (44, 264)
--
183 Name
193 m
212 Expr
216 b