-
- Downloads
Type checking and ADTs (#219)
Implements basis of a type system with type checking, ADTs. induction and more. Co-authored-by:SimonGuilloud <sim-guilloud@bluewin.ch> Co-authored-by:
Simon Guilloud <simon.guilloud@bluewin.ch> Co-authored-by:
Sankalp Gambhir <sankalp.gambhir42@gmail.com>
Showing
- .gitignore 2 additions, 0 deletions.gitignore
- CHANGES.md 4 additions, 0 deletionsCHANGES.md
- build.sbt 3 additions, 2 deletionsbuild.sbt
- lisa-examples/src/main/scala/ADTExample.scala 125 additions, 0 deletionslisa-examples/src/main/scala/ADTExample.scala
- lisa-sets/src/main/scala/lisa/Main.scala 3 additions, 0 deletionslisa-sets/src/main/scala/lisa/Main.scala
- lisa-sets/src/main/scala/lisa/automation/Apply.scala 141 additions, 121 deletionslisa-sets/src/main/scala/lisa/automation/Apply.scala
- lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala 1 addition, 1 deletionlisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
- lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala 10 additions, 8 deletionslisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala 535 additions, 0 deletions...rc/main/scala/lisa/maths/settheory/types/TypeSystem.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala 566 additions, 0 deletions.../main/scala/lisa/maths/settheory/types/adt/Frontend.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Functions.scala 134 additions, 0 deletions...main/scala/lisa/maths/settheory/types/adt/Functions.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala 1030 additions, 0 deletions...c/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala 174 additions, 0 deletions...c/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Typed.scala 285 additions, 0 deletions...src/main/scala/lisa/maths/settheory/types/adt/Typed.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala 1752 additions, 0 deletions...c/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
- lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/package.scala 200 additions, 0 deletions...c/main/scala/lisa/maths/settheory/types/adt/package.scala
- lisa-utils/src/main/scala/lisa/fol/Common.scala 132 additions, 13 deletionslisa-utils/src/main/scala/lisa/fol/Common.scala
- lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala 2 additions, 0 deletionslisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
- lisa-utils/src/main/scala/lisa/fol/Lambdas.scala 1 addition, 1 deletionlisa-utils/src/main/scala/lisa/fol/Lambdas.scala
- lisa-utils/src/main/scala/lisa/fol/Sequents.scala 4 additions, 4 deletionslisa-utils/src/main/scala/lisa/fol/Sequents.scala
Loading
Please register or sign in to comment