Skip to content

Instantly share code, notes, and snippets.



Last active Aug 31, 2016
What would you like to do?
I want this in Agda
-- This isn't real Agda code, but it's
-- something i find i want to have regularly.
-- As a simple example, the Integers.
data Int : Set where
ze : Int
su : Int -> Int
- (su x) : Int -> Int
- _ ()
su (- x) ()

This comment has been minimized.

Copy link
Owner Author

@bishboria bishboria commented Aug 31, 2016

The first - case ensures that any negative number must have a su as it's head constructor.

The last - case avoids both - ze and - (- x)

The second su case excludes any ways of putting a - in non head positions, avoiding
degenerate things like su (- (su (- (su ze))

Trying to push the idea of correct by construction to blend functions and data type declarations.

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