symmetric monoidal categories satisfy the other hexagon #3570
Annotations
2 warnings
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./test/Tactics/napply.v", line 16, characters 44-57:
Warning: Tactic Notation nrapply (uconstr) is deprecated since 2025-03-11.
nrapply was renamed to napply and will be removed soon
[deprecated-tactic-notation-since-2025-03-11,deprecated-since-2025-03-11,deprecated-tactic-notation,deprecated,default]
|
Run coq-community/docker-coq-action@v1
Could not find a terminator for warning:
File "./test/Tactics/napply.v", line 17, characters 44-58:
Warning: Tactic Notation snrapply (uconstr) is deprecated since 2025-03-11.
snrapply was renamed to snapply and will be removed soon
[deprecated-tactic-notation-since-2025-03-11,deprecated-since-2025-03-11,deprecated-tactic-notation,deprecated,default]
test/Tactics/napply.vo (real: 0.11, user: 0.05, sys: 0.06, mem: 143128 ko)
test/WildCat/Opposite.vo (real: 0.26, user: 0.16, sys: 0.09, mem: 355628 ko)
theories/Tactics/EquivalenceInduction.vo (real: 0.55, user: 0.46, sys: 0.08, mem: 361392 ko)
theories/Axioms/Univalence.vo (real: 0.09, user: 0.03, sys: 0.05, mem: 105072 ko)
theories/Classes/implementations/ne_list.vo (real: 0.13, user: 0.07, sys: 0.06, mem: 162052 ko)
theories/Functorish.vo (real: 0.11, user: 0.05, sys: 0.06, mem: 136944 ko)
theories/Spaces/BinInt/Core.vo (real: 0.13, user: 0.07, sys: 0.06, mem: 156276 ko)
theories/Types.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 111468 ko)
theories/Cubical/PathCube.vo (real: 3.15, user: 3.05, sys: 0.09, mem: 436372 ko)
theories/Colimits/Coeq.vo (real: 1.40, user: 1.31, sys: 0.09, mem: 382024 ko)
theories/Universes/TruncType.vo (real: 0.26, user: 0.17, sys: 0.08, mem: 355644 ko)
theories/Spaces/Nat/Arithmetic.vo (real: 0.18, user: 0.11, sys: 0.07, mem: 211696 ko)
theories/HIT/Flattening.vo (real: 0.38, user: 0.30, sys: 0.07, mem: 358516 ko)
theories/WildCat/Adjoint.vo (real: 0.56, user: 0.48, sys: 0.07, mem: 371872 ko)
theories/Spaces/Nat/Division.vo (real: 0.64, user: 0.56, sys: 0.07, mem: 367024 ko)
theories/Categories/Functor/Paths.vo (real: 0.34, user: 0.25, sys: 0.08, mem: 357928 ko)
theories/Categories/NaturalTransformation/Paths.vo (real: 0.18, user: 0.11, sys: 0.06, mem: 247664 ko)
theories/Categories/InitialTerminalCategory/Core.vo (real: 0.12, user: 0.06, sys: 0.06, mem: 135332 ko)
theories/WildCat/Products.vo (real: 1.81, user: 1.72, sys: 0.08, mem: 407272 ko)
theories/Categories/Functor/Prod/Universal.vo (real: 0.19, user: 0.11, sys: 0.07, mem: 253260 ko)
theories/Categories/SetCategory/Core.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 159732 ko)
theories/Categories/Functor/Composition/Laws.vo (real: 0.29, user: 0.21, sys: 0.07, mem: 355852 ko)
theories/Categories/NaturalTransformation/Dual.vo (real: 0.10, user: 0.04, sys: 0.05, mem: 106064 ko)
theories/Categories/Functor/Sum.vo (real: 0.28, user: 0.20, sys: 0.07, mem: 357572 ko)
theories/Categories/GroupoidCategory/Dual.vo (real: 0.15, user: 0.08, sys: 0.07, mem: 169108 ko)
theories/Categories/SetCategory/Morphisms.vo (real: 0.23, user: 0.15, sys: 0.08, mem: 272668 ko)
theories/Categories/SetCategory/Functors/SetProp.vo (real: 0.13, user: 0.06, sys: 0.06, mem: 133324 ko)
theories/Categories/Profunctor/Core.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 115116 ko)
theories/Categories/ExponentialLaws/Tactics.vo (real: 0.11, user: 0.06, sys: 0.05, mem: 110956 ko)
theories/Categories/Adjoint/UnitCounit.vo (real: 0.14, user: 0.07, sys: 0.06, mem: 182164 ko)
theories/Categories/Grothendieck/ToSet/Core.vo (real: 0.15, user: 0.08, sys: 0.06, mem: 166684 ko)
theories/Categories/CategoryOfSections/Core.vo (real: 0.14, user: 0.07, sys: 0.07, mem: 167128 ko)
theories/Categories/Structure/Core.vo (real: 0.16, user: 0.10, sys: 0.06, mem: 208656 ko)
theories/Metatheory/Core.vo (real: 0.10, user: 0.05, sys: 0.05, mem: 127532 ko)
theories/ExcludedMiddle.vo (real: 0.13, user: 0.06, sys: 0.06, mem: 147648 ko)
theories/Spaces/Pos.vo (real: 0.10, user: 0.04, sys: 0.05, mem: 108496 ko)
theories/Cubical/DPathCube.vo (real: 0.40, user: 0.32, sys: 0.08, mem: 359944 ko)
test/bugs/github1382.vo (real: 0.12, user: 0.06, sys: 0.05, mem: 134904 ko)
test/bugs/github726.vo (real: 0.11, user: 0.05, sys: 0.05, mem: 125680 ko)
theories/Classes/interfaces/ua_algebra.vo (real: 0.17, user: 0.10, sys: 0.06, mem: 200792 ko)
theories/Algebra/Universal/Algebra.vo (real: 0.38, user: 0.30, sys: 0.07, mem: 356396 ko)
theories/Diagrams/Diagram.vo (real: 0.23, user: 0.14, sys: 0.08, mem: 319280 ko)
theories/Colimits/CoeqUnivProp.vo (real: 0.43, user: 0.34, sys
|
Loading