Skip to content

Instantly share code, notes, and snippets.

@lenary

lenary/gcounter.idr

Forked from mrb/cong.idr
Created June 25, 2014 14:31
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save lenary/0eaee9cef15d823f2c34 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save lenary/0eaee9cef15d823f2c34 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. @mrb mrb revised this gist Jun 25, 2014. 1 changed file with 6 additions and 1 deletion.
    7 changes: 6 additions & 1 deletion gcounter.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -15,4 +15,9 @@ gc2 : GCounter
    gc2 = (MkGCounter 2)

    instance JoinSemilattice GCounter where
    join = gcjoin
    join = gcjoin

    instance VerifiedJoinSemilattice GCounter where
    joinSemilatticeJoinIsAssociative = ?a
    joinSemilatticeJoinIsCommutative = ?c
    joinSemilatticeJoinIsIdempotent = ?i
  2. @mrb mrb created this gist Jun 25, 2014.
    18 changes: 18 additions & 0 deletions gcounter.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,18 @@
    module Main

    import Prelude.Algebra

    record GCounter : Type where
    MkGCounter : (value : Int) -> GCounter

    gcjoin : GCounter -> GCounter -> GCounter
    gcjoin l r = (MkGCounter ((value l) + (value r)))

    gc1 : GCounter
    gc1 = (MkGCounter 1)

    gc2 : GCounter
    gc2 = (MkGCounter 2)

    instance JoinSemilattice GCounter where
    join = gcjoin