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
266 AbsToCon
327 AbsToCon b
373 a
591 Type
749 LiftedRep
2041 'Many
total (2034, 13705)
--
7 Doc
7 MonadAbsToCon m
8 Type -> Type
8 ToConcrete a
10 HasOptions m
12 ConOfAbs a
14 a
14 Type
25 m
33 'Many
total (51, 233)
--
190 Type -> Type
222 m1
263 Bool
349 Term
350 Type
357 TCMT IO
709 Expr
938 LiftedRep
1068 m
1800 'Many
total (1638, 15498)
--
176 Semigroup (m Doc)
181 IsString (m Doc)
195 PureTCM m
196 MonadFresh NameId m
197 MonadInteractionPoints m
218 HasOptions m
220 Type -> Type
381 m Doc
585 m
611 'Many
total (819, 6559)
--
1 [Doc]
1 [ProblemConstraint]
1 Module
1 Doc
1 PrettyTCM ProblemConstraint
1 MonadPretty m
2 m
2 Type
3 ProblemConstraint
4 'Many
total (17, 24)
--
14 IsString (m Doc)
16 QName
16 HasOptions m
19 m1
35 'Many
36 [m Doc]
42 []
100 LiftedRep
227 m
270 m Doc
total (148, 1191)
--
31 Nat
40 Bool
41 Type
41 TCMT IO
43 ConHead
51 Term
64 QName
100 LiftedRep
152 m
408 'Many
total (223, 1936)
--
56 NamesT m
64 b
66 ReaderT Names m
70 [String]
81 AbsN a
256 a
262 Type -> Type
311 Type
508 m
699 'Many
total (739, 4156)
--
29 Applicative m
29 QName
30 m Term
45 Type
48 String
49 Type -> Type
49 LiftedRep
106 Term
111 m
250 'Many
total (231, 1383)
--
63 FamilyOrNot a
64 TCMT IO
68 NamesT m
81 ReduceM
91 a
101 Type
103 LiftedRep
127 m
241 Term
411 'Many
total (383, 2789)
--
28 CallStack
29 Int
31 Type
76 LiftedRep
82 QuotingKit
114 ReduceM Term
128 TCMT IO
139 ReduceM
356 'Many
412 Term
total (280, 2199)
--
41 NamesT ReduceM Term
48 NamesT (TCMT IO) Term
73 ReduceM
88 NamesT ReduceM
99 Arg Term
101 TCMT IO
105 NamesT (TCMT IO)
148 'Many
193 LiftedRep
212 Term
total (132, 1668)
--
43 Maybe Term
74 NamesT (TCMT IO)
96 NamesT m Term
106 TCMT IO
109 m
133 Arg Term
168 LiftedRep
197 'Many
222 NamesT m
261 Term
total (133, 2077)
--
47 Maybe Term
74 NamesT m Term
76 NamesT (TCMT IO)
85 TCMT IO
94 Arg Term
106 m
108 LiftedRep
169 'Many
182 NamesT m
258 Term
total (137, 1791)
--
140 NamesT (ExceptT (Closure (Abs Type)) m)
145 Type
174 NamesT ReduceM
210 ReduceM
220 TCMT IO
257 Arg Term
288 m
649 LiftedRep
1137 Term
1206 'Many
total (916, 9881)
--
146 Integer
146 TCM PrimitiveImpl
155 Arg Term
185 Type
204 Nat
215 Double
438 TCMT IO
453 Term
467 LiftedRep
993 'Many
total (851, 7565)
--
54 Integer
54 Type
58 (# #)
59 TAlt
69 TPrim
89 Atom
95 ReaderT SEnv Identity
131 LiftedRep
406 TTerm
443 'Many
total (281, 2543)
--
6 CallStack
7 IO
8 Maybe QName
8 TAlt
8 CaseType
9 BuiltinKit
10 KindRep
11 TCMT IO
16 TTerm
20 'Many
total (38, 148)
--
53 LiftedRep
54 Modality
55 m Bool
55 Type -> Type
69 Bool
89 Term
89 TCMT IO
111 Type
212 m
515 'Many
total (475, 2679)
--
89 Int
90 Bool
100 TCMT IO Doc
136 QName
144 Type
170 TCMT IO
268 Term
324 LiftedRep
424 m
779 'Many
total (744, 5733)
--
9 Dom (ArgName, Type)
10 TCMT IO Doc
12 ArgName
13 Clause
14 Type
15 IO
18 'Many
23 Term
24 LiftedRep
35 TCMT IO
total (91, 331)
--
79 m1
82 Nat
88 QName
101 Node
110 a
143 Type
185 OccurrencesBuilder
239 LiftedRep
239 TCMT IO
721 'Many
total (696, 5183)
--
41 Type -> Type
43 Name
49 String
58 [TCWarning]
116 []
131 [m Doc]
231 LiftedRep
257 'Many
394 m Doc
426 m
total (394, 3228)
--
34 ()
36 TCMT IO Doc
47 TCMT IO ()
59 Bool
69 Type
102 m
115 TCMT IO
127 Term
167 LiftedRep
313 'Many
total (280, 2062)
--
13 Level
14 CallStack
17 IO
24 Type
26 Int
35 Type
39 LiftedRep
57 TCMT IO
65 Term
94 'Many
total (164, 757)
--
76 LiftedRep
77 LeftoverPatterns
86 FlexibleVar a
87 String
106 b
130 a
138 m
189 KindRep
233 Type
550 'Many
total (646, 3976)
--
22 WithOrigin (Ranged ArgName)
25 m1
31 Type
43 Type
49 TCMT IO
50 TCMT IO Doc
65 Term
78 LiftedRep
95 m
165 'Many
total (307, 1503)
--
16 Type
20 Type
22 NamedArg Pattern
28 Term
30 TCMT IO
35 [NamedArg Pattern]
39 TCMT IO Doc
47 LiftedRep
63 m
67 'Many
total (179, 761)
--
18 Pattern
22 m
22 IO
24 ExpandPatternSynonyms a<