← Back

Modules

Leios

  • Abstract
  • Base
  • Blocks
  • Config
  • FFD
  • KeyRegistration
  • Linear
  • Linear.Trace.Verifier
  • Linear.Trace.Verifier.Test
  • Prelude
  • Protocol
  • SpecStructure
  • Voting
  • VRF

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