aboutsummaryrefslogtreecommitdiff
path: root/.github/workflows
diff options
context:
space:
mode:
authorJosh Chen2020-08-14 11:07:17 +0200
committerJosh Chen2020-08-14 11:07:17 +0200
commitbd2efacaf67ae84c41377e7af38dacc5aa64f405 (patch)
tree7f213a432b28fc40cb8554bf13bb576f056f2bb7 /.github/workflows
parent8f4ff41d24dd8fa6844312456d47cad4be6cb239 (diff)
(FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules.
(REF) Goal statement assumptions are now put into the new context data slots. (FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data. (REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context. MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`. (REF) Fixed incompatibilities in theories.
Diffstat (limited to '.github/workflows')
0 files changed, 0 insertions, 0 deletions