Differentiation of TermS and Subst#49
Conversation
|
I merged the other PR, please rebase this one on top of current master and I'll review it. |
src/Agda/Core/Syntax.agda
Outdated
| data Branches α where | ||
| BsNil : Branches α mempty | ||
| BsCons : Branch α c → Branches α cs → Branches α (c ◃ cs) | ||
| BsCons : Branch α c → Branches α cs → Branches α (cs ▸ c) |
There was a problem hiding this comment.
Why would you use RScope here? It doesn't really make sense to me since the new branch is added on the left.
There was a problem hiding this comment.
I didn't use RScope here, this is the notation for Scope, the notation for RScope is x ◂ rβ.
I kept the previous datatype. (It's very confusing because the new notation for Scope is cs ▸ c and the previous one was c ◃ cs)
There was a problem hiding this comment.
Ah, well then I think this is a good opportunity to also use RScope :)
There was a problem hiding this comment.
It was a bigger change than I would have thought. I had to make some changes in the Scope library.
|
Thank you! I have a few small remarks, but otherwise this looks very good. |
|
The last commit depends on a new PR in Scope. |
|
This is still marked as a draft, but I assume it's ready now? |
|
Yes, I noted it as a draft so that it wouldn't be merged before updating flake.nix to add the last PR in Scope. |
* TypeS * Changes in Typing rules * TypeChecker updated * begin update of unification * partial refactoring using RScope * changes up to Typechecker * agda code fully updated with RScope * fix test file * moving renaming helpers from unification to unifier * update RScope and Scope up to substitute * update RScope and Scope all files * fixing Haskell * notations * evalCon and evalData * remove commented code * update Scope lib * fix Haskell * added tyBBranch' to fix a strange extraction bug probably linked to record types * fix ToCore.hs * corrections * whitespace * RScope in Branches * update scope
2 participants
Trying to split the Subst datatype into a datatype for Substitutions and one for arguments. And adding the notion of RScope instead of reversing Scope.