← Back

Modules

Leios

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

Network

  • BasicBroadcast
1234567891011121314
{-# OPTIONS --cubical-compatible #-}
module Class.Show.Core where
 
open import Class.Prelude
open import Class.Core
 
record Show (A : Type ℓ) : Type ℓ where
constructor mkShow
field show : A → String
open Show ⦃...⦄ public
 
Show¹ = Show ¹
Show² = Show ²
Show³ = Show ³