Skip to content
This repository has been archived by the owner on May 20, 2018. It is now read-only.

Generic eliminators/pattern matching #76

Closed
robrix opened this issue Jun 7, 2015 · 3 comments
Closed

Generic eliminators/pattern matching #76

robrix opened this issue Jun 7, 2015 · 3 comments
Labels
enhancement

Comments

@robrix
Copy link
Contributor

robrix commented Jun 7, 2015

This is an extension to type descriptions.

cf #65.
@robrix
Copy link
Contributor Author

robrix commented Oct 11, 2015

We introduce data constructors correctly, now we need to introduce eliminators.

@robrix robrix changed the title Generic constructors & eliminators Generic eliminators/pattern matching Oct 11, 2015
@robrix
Copy link
Contributor Author

robrix commented Oct 11, 2015

An example of how we might expect this to look:

data Natural : Type where
    zero : Natural
    successor : Natural → Natural

isZero : Natural → Boolean
    = λ n : Natural . case n (λ _ : Unit . true) (λ _ : Natural . λ _ : Unit . false)

(Remembering that constructed values are currently represented as right-nested tuples terminated with the unit value.)

@robrix
Copy link
Contributor Author

robrix commented Oct 24, 2015

This was done in #142 via the encoding of datatypes as functions serving as their eliminators.

@robrix robrix closed this as completed Oct 24, 2015
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@robrix