Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Produce eta-normal proofs #28

Open
RichardMoot opened this issue Apr 25, 2015 · 0 comments
Open

Produce eta-normal proofs #28

RichardMoot opened this issue Apr 25, 2015 · 0 comments
Assignees
@RichardMoot
Labels
enhancement
Milestone
Version One

Comments

@RichardMoot
Copy link
Owner

Currently, the proof output produces long normal form proofs (ie. beta-normal eta-long proofs). This makes sense from the point of view of proof search, but can be more user-friendly to produce eta-normal proofs as well.

Add an (optional) proof transformation step which transforms long normal form proofs into beta-eta-normal proofs.
@RichardMoot RichardMoot added this to the Version One milestone Apr 25, 2015
@RichardMoot RichardMoot self-assigned this Apr 25, 2015
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RichardMoot RichardMoot

Labels
enhancement
Projects
None yet
Milestone
Version One
Development

No branches or pull requests
1 participant
@RichardMoot