Isabelle-HoTT/spartan, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 rename things + some small changes 2021-01-31T02:54:51+00:00 Josh Chen 2021-01-31T02:54:51+00:00 2feb56660700af107abb5a28a7120052ac405518 






renamings
2021-01-21T00:52:13+00:00

Josh Chen

2021-01-21T00:52:13+00:00

aff3d43d9865e7b8d082f0c239d2c73eee1fb291












Bugfix: no longer repeatedly add duplicate rules to simpset
2021-01-19T02:18:44+00:00

Josh Chen

2021-01-19T02:18:44+00:00

549f1d46884d068ebf18f76bb359624510b086b0












Swapped notation for metas (now ?) and holes (now {}), other notation and name changes.
2021-01-18T23:49:13+00:00

Josh Chen

2021-01-18T23:49:13+00:00

f46df86db9308dde29e0e5f97f54546ea1dc34bf












Basic experiments adding reduction to the type checker
2020-09-23T15:03:42+00:00

Josh Chen

2020-09-23T15:03:42+00:00

3922e24270518be67192ad6928bb839132c74c07












minor
2020-08-14T17:55:38+00:00

Josh Chen

2020-08-14T17:55:38+00:00

77df99b3ffa41395ced31785074525c85e35fee9












reorganize
2020-08-14T09:21:59+00:00

Josh Chen

2020-08-14T09:21:59+00:00

d172f9d35a9a1680ec15e4c61e5becbbc92d2ce7












(FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules.
2020-08-14T09:07:17+00:00

Josh Chen

2020-08-14T09:07:17+00:00

bd2efacaf67ae84c41377e7af38dacc5aa64f405

(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.





(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.







(FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step
2020-08-09T16:34:58+00:00

Josh Chen

2020-08-09T16:34:58+00:00

8f4ff41d24dd8fa6844312456d47cad4be6cb239












1. fix intros method. 2. Couple extra lemmas; good small test cases for normalization in typechecking/elaboration.
2020-08-05T13:21:43+00:00

Josh Chen

2020-08-05T13:21:43+00:00

c530305cbcafba9f66f1a55a1b5177a62f52535c