Skip to content

Instantly share code, notes, and snippets.

@lenary

lenary/Error

Last active August 29, 2015 14:03
Show Gist options
  • Save lenary/6c0bceecc06d6e38f7e8 to your computer and use it in GitHub Desktop.
Save lenary/6c0bceecc06d6e38f7e8 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Error
Idris> :l VerifiedNatLattice.idr
Type checking ./VerifiedNatLattice.idr
VerifiedNatLattice.idr:6:10:
When elaborating type of Prelude.Algebra.Nat instance of Prelude.Algebra.VerifiedBoundedJoinSemilattice, method boundedJoinSemilatticeBottomIsBottom:
Can't resolve type class BoundedJoinSemilattice B
Metavariables: Nat instance of Prelude.Algebra.VerifiedBoundedJoinSemilattice
Raw
VerifiedNatLattice.idr
instance VerifiedJoinSemilattice Nat where
joinSemilatticeJoinIsIdempotent = maximumIdempotent
joinSemilatticeJoinIsCommutative = maximumCommutative
joinSemilatticeJoinIsAssociative = maximumAssociative
instance VerifiedBoundedJoinSemilattice Nat where
boundedJoinSemilatticeBottomIsBottom = maximumZeroNLeft
@lenary
Copy link
Author

lenary commented Jul 14, 2014

Relevant Prelude Code (from Prelude.Algebra): https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Algebra.idr#L179-L198

Though, it's worth pointing out, the type of boundedJoinSemilatticeBottomIsBottom should be:

total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e

(because bottom is unitary, not nullary) see issue: idris-lang/Idris-dev#1384

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment