← Back

Modules

Leios

  • Linear

Network

  • BasicBroadcast
1234567891011
{-# OPTIONS --cubical-compatible #-}
 
module Class.CommutativeMonoid.Instances where
 
open import Class.CommutativeMonoid.Core
 
open import Data.Nat.Properties
 
module NonUniqueInstances where
CommMonoid-ℕ-+ = Conversion.fromBundle +-0-commutativeMonoid
CommMonoid-ℕ-* = Conversion.fromBundle *-1-commutativeMonoid