Open
Conversation
* ci: update permissions of runAll.sh * misc: remove last parts of lisa-sets2 * chore: fix documentation typos in Relations.Definitions * lib: prove that the Cartesian product is monotonic * lib: update definitions of injectivity and surjectivity * lib: define non-strict total orders * lib: rename some theorems * lib: rename initialSegment to predecessors * lib: prove that the membership relation is monotonic * misc: rename Ind to Set * feat: define classes, class functions, and bounded quantifiers * lib: prove well-ordered recursion, add more files * fix: bug for definitions with no free variables * ci: update runAll * lib: some more files * ci: add runAll to CI * lib: remove redundant theorem * lib: rename Order.Theorems to Order.BasicTheorems * lib: update comment --------- Co-authored-by: Simon Guilloud <simon.guilloud@bluewin.ch>
* Add doc with throws for mostRecentStep * Cleanup sorucecode implicits for helpers; only top level functions should create them * Remove extraction of data from sourcecode objects * Add type for public val * Split makeEq requires into two for better reporting
* Run tex-fmt, update gitignore * Update example files and instructions * Update chapter 1
* Make subproof return a more specific error when empty * Remove unused duplicate Subproof object * Add assumeAll, assumeAllSplit * Document helpers and clarify errors for empty proofs * scalafmt
* Remove Set alias within SetTheory * Change Set -> Ind in Example as well
* add a rewrite function that replace all occurences of a term by another in a third. * Removed Beta that was deprecated, fixed some sc-tptp tests, fixed some compilation warnings.
…er of proof lines shown in errors, add helper to show sorry dependencies of theorems.
SimonGuilloud
force-pushed
the
smallfixes
branch
from
76144c6 to
5b0e8fa
Compare
…er (epfl-lara#253) * update .gitignore * upload current progress * have some steps further * Substitute failed at TApp * fix Pi definition error and finish TApp prove * finish T-Abs set boundary check * Finish T-Abs functionality proof * Finish TAbs typing rule proof * Fix the error from abs defintion * Refactor the code * finish proving beta reduction * FIx the definition of Pi * provide some examples * Basic typing system with dependent type works! * Add more readable syntax and examples * add a new example * feat: Enhance Set Theory Library with Cardinality Definitions and Universe Structure - Added Cardinal.scala to define cardinality concepts including equinumerosity and dominance. - Introduced Universe.scala to establish the structural definition of Tarski/Grothendieck Universes. - Implemented UniverseRank.scala to define the level of a universe and its properties. - Created Predef.scala to export essential definitions from the cardinal package. - Updated Helper.scala, Examples.scala, Symbols.scala, and TypingRules.scala to integrate new cardinality and universe functionalities. - Added new theorems related to universes and cardinalities, including Cantor's theorem and the structure of universes. * draft for a strong universe * Finish the foundamental theorem(replacementImpliesFunctionRange)'s proof * feat: Add new theorems for universe closure properties and enhance Symbols with proposition variable * refactor: Simplify theorem definitions and remove commented-out universe structure theorem * feat: Enhance typing rules and tactics with new theorems for universe handling and subset relations * feat: replace the TForm with two auxilliary theorems within tactics * refactor: change the project name * feat: Add README file for LISA-CoC module with project overview and setup instructions * fix: adjust compiler options * Introduce subtyping case into current system, support automatical type-lifting * Add a new case study * Clean up, introduce a more reader-friendly notation for app operator * remove unused 'lisa-coc' project from build configuration
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
4 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.
No description provided.