Group theory Merge Conflict Resolution#1
Open
sankalpgambhir wants to merge 13 commits intodhalilov:mainfrom
Open
Group theory Merge Conflict Resolution#1sankalpgambhir wants to merge 13 commits intodhalilov:mainfrom
sankalpgambhir wants to merge 13 commits intodhalilov:mainfrom
Conversation
* Subst changes
* scala{fix, fmt}
Co-authored-by: SimonGuilloud <simon.guilloud@bluewin.ch>
* Sorry printing * Removed excessive pattern catchall --------- Co-authored-by: SimonGuilloud <simon.guilloud@bluewin.ch>
* Union of Relation/Function Set
* Pair singleton functional
* Well ordered induction
* scala{fix, fmt}
* Proof debugging
* Assumption handling fix for UniqueComprehension
* Well Ordered Induction
* scala{fix, fmt}
* Remove local sorry def
* Well ordered induction (stronger); fix assumptions
* Induction documentation
* continued induction proof
* Proof templates; the recursion proof moves along
* Added proof of transfinite induction with missing lemmas
* Inclusion anti symmetric
* Elements of ordinals are ordinals
* Clean up inductive part of well ordered recursion; redo proof structure
* Domain of Relational Union
* Change lemmas to theorems to force printing
* scalafix
* Added lemmas
* scalafix
* WO Recursion Uniqueness Proof
* Existence Proof Skeleton
* Restructure proof; partial union proof
* Function Subset Proof Outline
* Update to functional proof
* scalafix
* My first replacement proof (yay?)
* Limit and Successors for total orders, unions of initial segments
* Partial proof for limit case: functional part
* Pair in relation assumption fix
* Almost complete limit case proof for recursion
* Fix for ordered restriction definition
* Finish limit case
* Successor case skeleton
* More ordered restriction fixes
* Documentation cleanup
* Initial segment lemmas
* Proof debugging
* Partial successor case proof
* Successor case functional proof
* Beeg Refactoring
* scala{fix,fmt}
* Some proof debugging
* Recusrive property proof skeleton and partial
* scala{fix, fmt}
* uw = vpr
* Assume syntax fixes
* initial segment irreflexivity
* scala{fix,fmt}
* Restrictions equal
* Restrictions really equal
* appv = appw
* Much proof debugging
* Proof fixes
* scala{fix, fmt}
* Completed proof
* Wow passing proof can you imagine
* Formatting and doc
* Subst syntax change
* Much proof refactoring
---------
Co-authored-by: SimonGuilloud <simon.guilloud@bluewin.ch>
* Run `latexindent` * Auto convert all tabs to spaces * Cleanup before 1.2 * Updates till proof steps; trying to change to xelatex * latexindent --------- Co-authored-by: SimonGuilloud <simon.guilloud@bluewin.ch>
…eter Inference (epfl-lara#175) * match rewrite * Context discovery * scala{fix, fmt} * Documentation * Change to lazy subst checking * Change to lazy subst checking 2 * Subst proof non-working * Wow! a compiling version * Complete working subst * Move old subst to Substitution2 * Finishing up * Moving old unification utils * scalafix
* Update manual (Kernel) * fixed xelatex/bibtex issues, finished FOLAlg section, SC steps. Next: 1.2.2 Proofs * git add renamed files * Update title page, finished The kernel, currently half of Kernel's helpers. * Finished Kernel chapter, improvements to code presentation. * git add * Changes and formatting, part 1 * Auto-format + change to lstinline * Small changes --------- Co-authored-by: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
* Remove Substitution2
* Remove second order unifier, remove ref to first order unifier
* Remove UnificationUtils2
* scala{fix, fmt}
* Removed FIrstOrderUnifier
* Fix matching tests
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Reviewed the PR and merged epfl-lara/main into it, handling conflicts and making sure all theory files work as expected.