Adding support for untyped conversion-checking #64
+10,846
−4,589
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
removing the comparison between the types and endpoints for the equality eliminator (they are obtained by invariants instead) + general quality of life improvement
probably broken due to the changed def
admitted lemma for strengthening – for now
missing neutral cases + unproven injectivities in the universe
that escape at level zero is a terrible hack :(
this commit and the previous one don't make sense, but they are here to help git track things around
leaving deprecated direct usages of completeness
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR does quite a lot, but the base goal was to support the formalisation of an untyped conversion algorithm, basically that of Coq (with term-directed η for functions and pairs).
On the way of doing that, I tried to completely segregate the logical relation and its consequences from the "syntactic" consequences of these properties (eg SR as a consequence of injectivity of type constructors) and the "algorithmic" bit. So there is quite a large reorganisation, hopefully making the whole development more modular and structured. As a nice consequence, the algorithmic bit and logrel bits can now be compiled independently, as they are only put together in the very last file.
This is still somewhat a work in progress, I want to clean it up in the coming weeks. But it should be mostly stable by now.