Skip to content
New issue

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

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

Already on GitHub? # to your account

Rectification Campaign II: Restrictions, etc. #230

Merged
merged 64 commits into from
Aug 17, 2018
Merged

Conversation

jonsterling
Copy link
Collaborator

@jonsterling jonsterling commented Aug 14, 2018

Huge thanks to @ecavallo for exercising all the bugs fixed in this PR.

@jonsterling jonsterling changed the title Rectification [WIP] Rectification Campaign II: Restrictions, etc. [WIP] Aug 14, 2018
@jonsterling
Copy link
Collaborator Author

jonsterling commented Aug 14, 2018

Roadmap:

  • change the elaborator to push around restrictions in the same way that the typechecker does
  • hopefully, change the restriction pretypes to have an explicit intro and elim form

(* This is not backwards, FYI. *)
List.rev @@
(* ~~This is not backwards, FYI.~~ *)
(* NARRATOR VOICE: it was backwards. *)
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ecavallo 😆 😎

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I should be forbidden to use List.rev... I get so owned by it.

@jonsterling

This comment has been minimized.

@jonsterling jonsterling mentioned this pull request Aug 16, 2018
@ecavallo ecavallo mentioned this pull request Aug 17, 2018
@favonia
Copy link
Collaborator

favonia commented Aug 17, 2018

This should work:

let ncoe/int (n : int) : Path int (coe 0 1 n in λ _ → int) n = lam _ -> n

@jonsterling
Copy link
Collaborator Author

I think I will actually merge this now that it is cleaned up; the PR is getting too big.

@jonsterling jonsterling merged commit 510fa6a into master Aug 17, 2018
@jonsterling jonsterling deleted the rectification branch August 17, 2018 08:50
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
Projects
None yet
4 participants