mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 18:32:44 +03:00
16 lines
265 B
Idris
16 lines
265 B
Idris
module Algebra
|
|
|
|
import public Algebra.ZeroOneOmega
|
|
import public Algebra.Semiring
|
|
import public Algebra.Preorder
|
|
|
|
%default total
|
|
|
|
public export
|
|
RigCount : Type
|
|
RigCount = ZeroOneOmega
|
|
|
|
export
|
|
showCount : RigCount -> String
|
|
showCount = elimSemi "0 " "1 " (const "")
|