File tree Expand file tree Collapse file tree 1 file changed +1
-1
lines changed Expand file tree Collapse file tree 1 file changed +1
-1
lines changed Original file line number Diff line number Diff line change @@ -15,7 +15,7 @@ You can find the proof of type safety in [Soundness.thy](./Soundness.thy), the p
1515- [x] Use the Nominal2 framework to reason about alpha-equated terms ([ v2.0] ( https://github.com/jvanbruegge/isabelle-lambda-calculus/tree/v2.0 ) )
1616- [x] Extend to System F (ie introduce polymorphic variables) ([ v3.0] ( https://github.com/jvanbruegge/isabelle-lambda-calculus/tree/v3.0 ) )
1717- [x] Use a context validity judgement ([ v3.1] ( https://github.com/jvanbruegge/isabelle-lambda-calculus/tree/v3.1 ) )
18- - [x] Add arbitrary user-defined datatypes ([ v3.5 ] ( https://github.com/jvanbruegge/isabelle-lambda-calculus/tree/v3.5 ) )
18+ - [x] Add arbitrary user-defined datatypes ([ v3.6 ] ( https://github.com/jvanbruegge/isabelle-lambda-calculus/tree/v3.6 ) )
1919- [ ] Add ` case ` expressions
2020- [ ] Extend to System Fc (ie introduce type equality coercions)
2121- [ ] Extend to System FcPro (ie introduce kind abstractions)
You can’t perform that action at this time.
0 commit comments