Created
July 8, 2024 14:41
-
-
Save 4e554c4c/f5e747a299a7b619dcc88c0a81f464d6 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Checking Categories.Diagram.End.Fubini (<agda-categories>/src/Categories/Diagram/End/Fubini.agda). | |
| Statistics for Categories.Diagram.End.Fubini | |
| A.Name (fresh) 2,340 | |
| A.QName (fresh) 1,991 | |
| Double (fresh) 11 | |
| Integer (fresh) 2 | |
| Lazy Text (fresh) 666 | |
| Node (fresh) 25,761 | |
| Shared Term (fresh) 0 | |
| Strict Text (fresh) 1 | |
| Text (fresh) 41 | |
| attempted-constraints 175 | |
| compare 39,386 | |
| compare at eta record 8,308 | |
| compare at eta-record: eta-expanding 8,279 | |
| compare at eta-record: meta 29 | |
| compare at function type 1,881 | |
| compare by reduction 22,808 | |
| compare equal 4,577 | |
| compare levels 232 | |
| compare meta 2,532 | |
| compare meta shortcut 2,018 | |
| compare meta shortcut successful 2,017 | |
| compare sorts 34 | |
| icode () 4,688 | |
| icode (NameSpaceId,NameSpace) 651 | |
| icode (SerialisedRange,(TopLevelModuleName' (Range' (Maybe RangeFile))),Word64) 17 | |
| icode Abs (Tele (Dom' Term (Type'' Term Term))) 952 | |
| icode Abs (Type'' Term Term) 109 | |
| icode Abs Term 360 | |
| icode AbstractModule 203 | |
| icode AbstractName 2,026 | |
| icode Annotation 30,386 | |
| icode Arg (Named (WithOrigin (Ranged [Char])) (Pattern' DBPatVar)) 49 | |
| icode Arg (Named (WithOrigin (Ranged [Char])) (Ranged Int)) 167 | |
| icode Arg (Type'' Term Term) 4 | |
| icode Arg QName 1,713 | |
| icode Arg Term 26,969 | |
| icode Arg [Char] 53 | |
| icode ArgInfo 30,386 | |
| icode Aspect 1,238 | |
| icode Aspects 1,238 | |
| icode Associativity 4,366 | |
| icode Blocked' Term () 10 | |
| icode Bool 4,945 | |
| icode BoundVariablePosition 3 | |
| icode Clause 4 | |
| icode Cohesion 30,386 | |
| icode CompiledClauses' Term 4 | |
| icode ConHead 284 | |
| icode ConOrigin 284 | |
| icode CutOff 1 | |
| icode DBPatVar 49 | |
| icode DataOrRecord' PatternOrCopattern 284 | |
| icode DataOrRecordModule 119 | |
| icode Definition 10 | |
| icode DefinitionSite 732 | |
| icode Defn 10 | |
| icode Dom' Term (Type'' Term Term) 1,061 | |
| icode Double 648 | |
| icode Either ProjectionLikenessMissing Projection 4 | |
| icode Elim' Term 29,617 | |
| icode ExpandedEllipsis 4 | |
| icode FileType 1 | |
| icode Fixity 4,366 | |
| icode Fixity' 2,340 | |
| icode FixityLevel 4,366 | |
| icode FreeVariables 30,386 | |
| icode FunctionFlag 2 | |
| icode FunctionInverse' Clause 4 | |
| icode HashMap MetaId RemoteMetaVariable 1 | |
| icode HashMap QName Definition 1 | |
| icode HashMap QName [Open DisplayForm] 1 | |
| icode HashMap QName [RewriteRule] 1 | |
| icode Hiding 30,386 | |
| icode Induction 369 | |
| icode Int 38,007 | |
| icode Int32 36,106 | |
| icode IntSet 5,366 | |
| icode Integer 3,328 | |
| icode Interface 1 | |
| icode Interval' () 2,344 | |
| icode IsAbstract 4 | |
| icode IsOpaque 4 | |
| icode KindOfName 2,026 | |
| icode Language 10 | |
| icode Level' Term 1,163 | |
| icode Lock 30,386 | |
| icode Map ModuleName Scope 2 | |
| icode Map ModuleName Section 1 | |
| icode Map Name (NonEmpty AbstractModule) 651 | |
| icode Map Name (NonEmpty AbstractName) 651 | |
| icode Map OpaqueId OpaqueBlock 1 | |
| icode Map QName ([Arg Name],(Pattern' Void)) 1 | |
| icode Map QName ModuleName 217 | |
| icode Map QName Name 59 | |
| icode Map QName OpaqueId 1 | |
| icode Map QName Text 1 | |
| icode Map SomeBuiltin (Builtin (PrimitiveId,QName)) 1 | |
| icode Map [Char] ForeignCodeStack 1 | |
| icode Map [Char] [CompilerPragma] 10 | |
| icode Maybe (Arg (Type'' Term Term)) 4 | |
| icode Maybe (CompiledClauses' Term) 4 | |
| icode Maybe (SplitTree' SplitTag) 4 | |
| icode Maybe (Trie (NonEmpty Char) Int) 2 | |
| icode Maybe (WithOrigin (Ranged [Char])) 1,277 | |
| icode Maybe Aspect 1,238 | |
| icode Maybe Bool 16 | |
| icode Maybe ConfluenceCheck 1 | |
| icode Maybe Cubical 1 | |
| icode Maybe DataOrRecordModule 217 | |
| icode Maybe DefinitionSite 1,238 | |
| icode Maybe ExtLamInfo 4 | |
| icode Maybe Int 2 | |
| icode Maybe ModuleName 4 | |
| icode Maybe Name 26 | |
| icode Maybe NameKind 742 | |
| icode Maybe QName 19 | |
| icode Maybe RangeFile 4,714 | |
| icode Maybe Term 1,065 | |
| icode Maybe Text 1 | |
| icode Maybe [Char] 732 | |
| icode Maybe [QName] 4 | |
| icode Modality 30,386 | |
| icode ModuleName 3,418 | |
| icode ModuleNameHash 7,046 | |
| icode MutualId 10 | |
| icode Name 30,004 | |
| icode NameId 3,952 | |
| icode NameInScope 9,861 | |
| icode NameKind 742 | |
| icode NameMetadata 2,026 | |
| icode NamePart 11,512 | |
| icode NameSpace 651 | |
| icode NameSpaceId 651 | |
| icode Named (WithOrigin (Ranged [Char])) (Pattern' DBPatVar) 49 | |
| icode Named (WithOrigin (Ranged [Char])) (Ranged Int) 167 | |
| icode NonEmpty AbstractModule 203 | |
| icode NonEmpty AbstractName 2,026 | |
| icode NonEmpty NamePart 9,861 | |
| icode NonEmpty Text 3,094 | |
| icode NotBlocked' Term 10 | |
| icode NotationPart 283 | |
| icode NumGeneralizableArgs 10 | |
| icode Occurrence 26 | |
| icode OptionsPragma 2 | |
| icode Origin 31,490 | |
| icode PatOrigin 49 | |
| icode Pattern' DBPatVar 49 | |
| icode PatternInfo 49 | |
| icode PatternOrCopattern 284 | |
| icode PlusLevel' Term 2,112 | |
| icode Polarity 26 | |
| icode Position' () 4,688 | |
| icode PragmaOptions 1 | |
| icode ProfileOption 7 | |
| icode ProfileOptions 1 | |
| icode ProjLams 1 | |
| icode ProjOrigin 2,648 | |
| icode Projection 1 | |
| icode ProjectionLikenessMissing 3 | |
| icode QName 18,492 | |
| icode Quantity 30,386 | |
| icode QωOrigin 30,386 | |
| icode Range' (Maybe RangeFile) 20,500 | |
| icode RangeFile 2,344 | |
| icode RangeMap Aspects 1 | |
| icode Ranged BoundVariablePosition 3 | |
| icode Ranged Int 167 | |
| icode Ranged [Char] 1,217 | |
| icode Relevance 30,386 | |
| icode Scope 217 | |
| icode ScopeInfo 1 | |
| icode Section 58 | |
| icode SerialisedRange 2,357 | |
| icode Set FunctionFlag 4 | |
| icode Set OtherAspect 1,238 | |
| icode Set QName 662 | |
| icode Set WarningName 1 | |
| icode Signature 1 | |
| icode Sort' Term 1,248 | |
| icode SplitTree' SplitTag 2 | |
| icode Tele (Dom' Term (Type'' Term Term)) 1,014 | |
| icode Term 30,633 | |
| icode Text 9,493 | |
| icode TokenBased 1,238 | |
| icode TopLevelModuleName' (Range' (Maybe RangeFile)) 3,094 | |
| icode Type'' Term Term 1,184 | |
| icode Univ 1,216 | |
| icode WarningMode 1 | |
| icode WarningName 102 | |
| icode WhyInScope 6,396 | |
| icode WithDefault' Bool 'False 38 | |
| icode WithDefault' Bool 'True 20 | |
| icode WithDefault' UnicodeOrAscii 'True 1 | |
| icode WithOrigin (Ranged [Char]) 1,104 | |
| icode Word64 11,016 | |
| icode [(Name,LocalVar)] 2 | |
| icode [(NameSpaceId,NameSpace)] 217 | |
| icode [(SerialisedRange,(TopLevelModuleName' (Range' (Maybe RangeFile))),Word64)] 1 | |
| icode [Arg (Named (WithOrigin (Ranged [Char])) (Pattern' DBPatVar))] 4 | |
| icode [Arg QName] 284 | |
| icode [Arg [Char]] 5 | |
| icode [Char] 14,144 | |
| icode [Clause] 8 | |
| icode [Elim' Term] 6,298 | |
| icode [FunctionFlag] 4 | |
| icode [Int] 5,366 | |
| icode [Interval' ()] 2,357 | |
| icode [Maybe Name] 10 | |
| icode [ModuleName] 217 | |
| icode [Name] 3,467 | |
| icode [NotationPart] 2,340 | |
| icode [Occurrence] 10 | |
| icode [Open DisplayForm] 10 | |
| icode [OptionsPragma] 2 | |
| icode [OtherAspect] 1,238 | |
| icode [PlusLevel' Term] 1,163 | |
| icode [Polarity] 10 | |
| icode [Precedence] 1 | |
| icode [ProfileOption] 1 | |
| icode [QName] 666 | |
| icode [TCWarning] 1 | |
| icode [WarningName] 1 | |
| icode [[Char]] 2 | |
| max-open-constraints 18 | |
| metas 2,584 | |
| pointer equality: sorts 8 | |
| pointer equality: terms 12 | |
| pointers (fresh) 0 | |
| Total 561,198ms | |
| Miscellaneous 10ms | |
| Typing 2ms (552,271ms) | |
| Typing.CheckRHS 547,634ms | |
| Typing.Generalize 3,741ms | |
| Typing.OccursCheck 791ms | |
| Typing.TypeSig 88ms | |
| Typing.CheckLHS 12ms (12ms) | |
| Positivity 2,946ms | |
| DeadCode 0ms (1,833ms) | |
| DeadCode.DeadCodeInstantiateFull 1,831ms | |
| Termination 1,287ms (1,750ms) | |
| Termination.RecCheck 462ms | |
| Deserialization 1,244ms (1,677ms) | |
| Deserialization.Compaction 433ms | |
| Coverage 334ms (334ms) | |
| Serialization 295ms (306ms) | |
| Parsing 23ms (43ms) | |
| Parsing.OperatorsExpr 18ms | |
| Import 25ms | |
| Scoping 12ms (16ms) | |
| Accumulated statistics | |
| A.Name (fresh) 2,340 | |
| A.QName (fresh) 1,991 | |
| Double (fresh) 11 | |
| Integer (fresh) 2 | |
| Lazy Text (fresh) 666 | |
| Node (fresh) 25,761 | |
| Shared Term (fresh) 0 | |
| Strict Text (fresh) 1 | |
| Text (fresh) 41 | |
| attempted-constraints 175 | |
| compare 39,386 | |
| compare at eta record 8,308 | |
| compare at eta-record: eta-expanding 8,279 | |
| compare at eta-record: meta 29 | |
| compare at function type 1,881 | |
| compare by reduction 22,808 | |
| compare equal 4,577 | |
| compare levels 232 | |
| compare meta 2,532 | |
| compare meta shortcut 2,018 | |
| compare meta shortcut successful 2,017 | |
| compare sorts 34 | |
| icode () 4,688 | |
| icode (NameSpaceId,NameSpace) 651 | |
| icode (SerialisedRange,(TopLevelModuleName' (Range' (Maybe RangeFile))),Word64) 17 | |
| icode Abs (Tele (Dom' Term (Type'' Term Term))) 952 | |
| icode Abs (Type'' Term Term) 109 | |
| icode Abs Term 360 | |
| icode AbstractModule 203 | |
| icode AbstractName 2,026 | |
| icode Annotation 30,386 | |
| icode Arg (Named (WithOrigin (Ranged [Char])) (Pattern' DBPatVar)) 49 | |
| icode Arg (Named (WithOrigin (Ranged [Char])) (Ranged Int)) 167 | |
| icode Arg (Type'' Term Term) 4 | |
| icode Arg QName 1,713 | |
| icode Arg Term 26,969 | |
| icode Arg [Char] 53 | |
| icode ArgInfo 30,386 | |
| icode Aspect 1,238 | |
| icode Aspects 1,238 | |
| icode Associativity 4,366 | |
| icode Blocked' Term () 10 | |
| icode Bool 4,945 | |
| icode BoundVariablePosition 3 | |
| icode Clause 4 | |
| icode Cohesion 30,386 | |
| icode CompiledClauses' Term 4 | |
| icode ConHead 284 | |
| icode ConOrigin 284 | |
| icode CutOff 1 | |
| icode DBPatVar 49 | |
| icode DataOrRecord' PatternOrCopattern 284 | |
| icode DataOrRecordModule 119 | |
| icode Definition 10 | |
| icode DefinitionSite 732 | |
| icode Defn 10 | |
| icode Dom' Term (Type'' Term Term) 1,061 | |
| icode Double 648 | |
| icode Either ProjectionLikenessMissing Projection 4 | |
| icode Elim' Term 29,617 | |
| icode ExpandedEllipsis 4 | |
| icode FileType 1 | |
| icode Fixity 4,366 | |
| icode Fixity' 2,340 | |
| icode FixityLevel 4,366 | |
| icode FreeVariables 30,386 | |
| icode FunctionFlag 2 | |
| icode FunctionInverse' Clause 4 | |
| icode HashMap MetaId RemoteMetaVariable 1 | |
| icode HashMap QName Definition 1 | |
| icode HashMap QName [Open DisplayForm] 1 | |
| icode HashMap QName [RewriteRule] 1 | |
| icode Hiding 30,386 | |
| icode Induction 369 | |
| icode Int 38,007 | |
| icode Int32 36,106 | |
| icode IntSet 5,366 | |
| icode Integer 3,328 | |
| icode Interface 1 | |
| icode Interval' () 2,344 | |
| icode IsAbstract 4 | |
| icode IsOpaque 4 | |
| icode KindOfName 2,026 | |
| icode Language 10 | |
| icode Level' Term 1,163 | |
| icode Lock 30,386 | |
| icode Map ModuleName Scope 2 | |
| icode Map ModuleName Section 1 | |
| icode Map Name (NonEmpty AbstractModule) 651 | |
| icode Map Name (NonEmpty AbstractName) 651 | |
| icode Map OpaqueId OpaqueBlock 1 | |
| icode Map QName ([Arg Name],(Pattern' Void)) 1 | |
| icode Map QName ModuleName 217 | |
| icode Map QName Name 59 | |
| icode Map QName OpaqueId 1 | |
| icode Map QName Text 1 | |
| icode Map SomeBuiltin (Builtin (PrimitiveId,QName)) 1 | |
| icode Map [Char] ForeignCodeStack 1 | |
| icode Map [Char] [CompilerPragma] 10 | |
| icode Maybe (Arg (Type'' Term Term)) 4 | |
| icode Maybe (CompiledClauses' Term) 4 | |
| icode Maybe (SplitTree' SplitTag) 4 | |
| icode Maybe (Trie (NonEmpty Char) Int) 2 | |
| icode Maybe (WithOrigin (Ranged [Char])) 1,277 | |
| icode Maybe Aspect 1,238 | |
| icode Maybe Bool 16 | |
| icode Maybe ConfluenceCheck 1 | |
| icode Maybe Cubical 1 | |
| icode Maybe DataOrRecordModule 217 | |
| icode Maybe DefinitionSite 1,238 | |
| icode Maybe ExtLamInfo 4 | |
| icode Maybe Int 2 | |
| icode Maybe ModuleName 4 | |
| icode Maybe Name 26 | |
| icode Maybe NameKind 742 | |
| icode Maybe QName 19 | |
| icode Maybe RangeFile 4,714 | |
| icode Maybe Term 1,065 | |
| icode Maybe Text 1 | |
| icode Maybe [Char] 732 | |
| icode Maybe [QName] 4 | |
| icode Modality 30,386 | |
| icode ModuleName 3,418 | |
| icode ModuleNameHash 7,046 | |
| icode MutualId 10 | |
| icode Name 30,004 | |
| icode NameId 3,952 | |
| icode NameInScope 9,861 | |
| icode NameKind 742 | |
| icode NameMetadata 2,026 | |
| icode NamePart 11,512 | |
| icode NameSpace 651 | |
| icode NameSpaceId 651 | |
| icode Named (WithOrigin (Ranged [Char])) (Pattern' DBPatVar) 49 | |
| icode Named (WithOrigin (Ranged [Char])) (Ranged Int) 167 | |
| icode NonEmpty AbstractModule 203 | |
| icode NonEmpty AbstractName 2,026 | |
| icode NonEmpty NamePart 9,861 | |
| icode NonEmpty Text 3,094 | |
| icode NotBlocked' Term 10 | |
| icode NotationPart 283 | |
| icode NumGeneralizableArgs 10 | |
| icode Occurrence 26 | |
| icode OptionsPragma 2 | |
| icode Origin 31,490 | |
| icode PatOrigin 49 | |
| icode Pattern' DBPatVar 49 | |
| icode PatternInfo 49 | |
| icode PatternOrCopattern 284 | |
| icode PlusLevel' Term 2,112 | |
| icode Polarity 26 | |
| icode Position' () 4,688 | |
| icode PragmaOptions 1 | |
| icode ProfileOption 7 | |
| icode ProfileOptions 1 | |
| icode ProjLams 1 | |
| icode ProjOrigin 2,648 | |
| icode Projection 1 | |
| icode ProjectionLikenessMissing 3 | |
| icode QName 18,492 | |
| icode Quantity 30,386 | |
| icode QωOrigin 30,386 | |
| icode Range' (Maybe RangeFile) 20,500 | |
| icode RangeFile 2,344 | |
| icode RangeMap Aspects 1 | |
| icode Ranged BoundVariablePosition 3 | |
| icode Ranged Int 167 | |
| icode Ranged [Char] 1,217 | |
| icode Relevance 30,386 | |
| icode Scope 217 | |
| icode ScopeInfo 1 | |
| icode Section 58 | |
| icode SerialisedRange 2,357 | |
| icode Set FunctionFlag 4 | |
| icode Set OtherAspect 1,238 | |
| icode Set QName 662 | |
| icode Set WarningName 1 | |
| icode Signature 1 | |
| icode Sort' Term 1,248 | |
| icode SplitTree' SplitTag 2 | |
| icode Tele (Dom' Term (Type'' Term Term)) 1,014 | |
| icode Term 30,633 | |
| icode Text 9,493 | |
| icode TokenBased 1,238 | |
| icode TopLevelModuleName' (Range' (Maybe RangeFile)) 3,094 | |
| icode Type'' Term Term 1,184 | |
| icode Univ 1,216 | |
| icode WarningMode 1 | |
| icode WarningName 102 | |
| icode WhyInScope 6,396 | |
| icode WithDefault' Bool 'False 38 | |
| icode WithDefault' Bool 'True 20 | |
| icode WithDefault' UnicodeOrAscii 'True 1 | |
| icode WithOrigin (Ranged [Char]) 1,104 | |
| icode Word64 11,016 | |
| icode [(Name,LocalVar)] 2 | |
| icode [(NameSpaceId,NameSpace)] 217 | |
| icode [(SerialisedRange,(TopLevelModuleName' (Range' (Maybe RangeFile))),Word64)] 1 | |
| icode [Arg (Named (WithOrigin (Ranged [Char])) (Pattern' DBPatVar))] 4 | |
| icode [Arg QName] 284 | |
| icode [Arg [Char]] 5 | |
| icode [Char] 14,144 | |
| icode [Clause] 8 | |
| icode [Elim' Term] 6,298 | |
| icode [FunctionFlag] 4 | |
| icode [Int] 5,366 | |
| icode [Interval' ()] 2,357 | |
| icode [Maybe Name] 10 | |
| icode [ModuleName] 217 | |
| icode [Name] 3,467 | |
| icode [NotationPart] 2,340 | |
| icode [Occurrence] 10 | |
| icode [Open DisplayForm] 10 | |
| icode [OptionsPragma] 2 | |
| icode [OtherAspect] 1,238 | |
| icode [PlusLevel' Term] 1,163 | |
| icode [Polarity] 10 | |
| icode [Precedence] 1 | |
| icode [ProfileOption] 1 | |
| icode [QName] 666 | |
| icode [TCWarning] 1 | |
| icode [WarningName] 1 | |
| icode [[Char]] 2 | |
| max-open-constraints 18 | |
| metas 2,584 | |
| pointer equality: sorts 8 | |
| pointer equality: terms 12 | |
| pointers (fresh) 0 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment