cf0d17df57
[kernel-coq] Correct statement of subtyping consistency, extend to statements.
...
Bug:
Change-Id: I48f073fa592ccdac56fb63b33b7d9961be5fc3fe
Reviewed-on: https://dart-review.googlesource.com/8220
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com >
2017-09-27 13:39:05 +00:00
12c4b62be8
[kernel] Completion of consistency proofs for type system of first subset of kernel.
...
Bug:
Change-Id: I5ae6fa1ddbb79b6f9dfecb53762b7ee5660c9117
Reviewed-on: https://dart-review.googlesource.com/5746
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com >
2017-09-18 11:37:03 +00:00
184d1959c5
[kernel] Proofs about type equality, beginnings of the type checking homomorphism proof.
...
I also added mutual induction schemes for types and expressions.
Some changes from the "Cleanup" revision are in here as well because Gerrit is terrible.
Bug:
Change-Id: I0859a6c1cba8179e0a64cc0455ab2a83fad8f26b
Reviewed-on: https://dart-review.googlesource.com/5300
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com >
2017-09-13 12:00:19 +00:00
a71d91ea62
[kernel] Cleanup of object model and coq.dart.
...
Bug:
Change-Id: I4a93d2ab0a052b61d3819d04316c05f534057f02
Reviewed-on: https://dart-review.googlesource.com/5266
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com >
2017-09-13 11:43:30 +00:00
474c075794
[kernel] Simplified Coq AST and first draft of it's type system.
...
Details to come in discussions.
Bug:
Change-Id: Ia50d85dd27cde83e25086f64dc6746cc52036128
Reviewed-on: https://dart-review.googlesource.com/4941
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com >
2017-09-12 16:23:16 +00:00
Samir Jindel