Isabelle-HoTT/spartan/lib, 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












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












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







(REF) Tweak attribute names in preparation for new logical introduction rule behavior
2020-07-31T16:10:10+00:00

Josh Chen

2020-07-31T16:10:10+00:00

77aa10763429d2ded040071fbf7bee331dd52f5e












(FEAT) Term elaboration of assumption and goal statements.
2020-07-31T12:56:24+00:00

Josh Chen

2020-07-31T12:56:24+00:00

ff5454812f9e2720bd90c3a5437505644f63b487

  . spartan/core/goals.ML
  . spartan/core/elaboration.ML
  . spartan/core/elaborated_statement.ML

(FEAT) More context tacticals and search tacticals.
  . spartan/core/context_tactical.ML

(FEAT) Improved subgoal focus.
  Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
  . spartan/core/focus.ML

(FIX) Normalize facts in order to be able to resolve properly.
  . spartan/core/typechecking.ML

(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.





  . spartan/core/goals.ML
  . spartan/core/elaboration.ML
  . spartan/core/elaborated_statement.ML

(FEAT) More context tacticals and search tacticals.
  . spartan/core/context_tactical.ML

(FEAT) Improved subgoal focus.
  Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
  . spartan/core/focus.ML

(FIX) Normalize facts in order to be able to resolve properly.
  . spartan/core/typechecking.ML

(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.







1. Type-checking/inference now more principled, and the implementation is better. 2. Changed most tactics to context tactics.
2020-07-21T00:09:44+00:00

Josh Chen

2020-07-21T00:09:44+00:00

12eed8685674b7d5ff7bc45a44a061e01f99ce5f












Non-annotated object lambda
2020-07-09T11:35:39+00:00

Josh Chen

2020-07-09T11:35:39+00:00

831f33468f227c0dc96bd31380236f2c77e70c52












1. Initial `Definition` keyword. 2. ifelse.
2020-07-08T13:55:48+00:00

Josh Chen

2020-07-08T13:55:48+00:00

07c51b1801bd701bef61cedd571a944d9bd37e8b












rename folders
2020-06-15T09:52:19+00:00

Josh Chen

2020-06-15T09:52:19+00:00

69bf0744a5ce3ba144f59564ebf74d7d2f56b748