Summary:
Common datastructures used by both the Kernel AST definition and the object
model are factored into a shared module. A monad for partial computation is
defined to allow us to factor out termination proofs and syntactic validity
checks from the type checking and subtyping relations.
Test Plan:
Ran through coqc.
Bug:
Change-Id: I884666d7cc5b757d62541a46b868f8579a06f011
Reviewed-on: https://dart-review.googlesource.com/4700
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
Samir Jindel
95c5b043fb