Skip to content

Instantly share code, notes, and snippets.

@LeifW

LeifW/Smile.idr

Created April 30, 2020 21:43
Show Gist options
  • Save LeifW/c5b9713d979c97a90ded341b15cb3564 to your computer and use it in GitHub Desktop.
Save LeifW/c5b9713d979c97a90ded341b15cb3564 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Smile.idr
import Interfaces.Verified
%default total
data Face = Frown | Smile
Semigroup Face where
Smile <+> Smile = Smile
Smile <+> Frown = Frown
Frown <+> Smile = Frown
Frown <+> Frown = Frown
VerifiedSemigroup Face where
semigroupOpIsAssociative Frown Frown Frown = Refl
semigroupOpIsAssociative Frown Frown Smile = Refl
semigroupOpIsAssociative Frown Smile Frown = Refl
semigroupOpIsAssociative Frown Smile Smile = Refl
semigroupOpIsAssociative Smile Frown Frown = Refl
semigroupOpIsAssociative Smile Frown Smile = Refl
semigroupOpIsAssociative Smile Smile Frown = Refl
semigroupOpIsAssociative Smile Smile Smile = Refl
Monoid Face where
neutral = Smile
VerifiedMonoid Face where
monoidNeutralIsNeutralL Frown = Refl
monoidNeutralIsNeutralL Smile = Refl
monoidNeutralIsNeutralR Frown = Refl
monoidNeutralIsNeutralR Smile = Refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment