Isabelle-HoTT/hott, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 https://stuebinm.eu/git/Isabelle-HoTT/atom/hott?h=master 2022-06-28T23:28:53Z (broken) update hott for Isabelle 2021-1 2022-06-28T23:28:53Z stuebinm 2022-06-28T23:28:53Z urn:sha1:4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d this just replaces all instance of `this` with instances of `infer`. Unfortunately, it looks likes something else also broke, and I have no idea what it is (but the proof for equiv_if_equal fails). Sadly this means we can't get to univalence for now … (but rn I'm too tired to try anything else with it) 1. Thm/def statement display. 2. Syntax + computation proof. 2021-06-28T15:06:19Z Josh Chen 2021-06-28T15:06:19Z urn:sha1:5655750e12d3459c1237588f8dec3fc883a966b7 begin refactoring Equivalence 2021-06-28T12:34:31Z Josh Chen 2021-06-28T12:34:31Z urn:sha1:06f38e1bad882ec85cbfd89b74feef380c8bbd69 Bad practice huge commit: 2021-06-24T21:40:05Z Josh Chen 2021-06-24T21:40:05Z urn:sha1:f988d541364841cd208f4fd21ff8e5e2935fc7aa 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file Patch proof. Now works on Isabelle2021. 2021-04-17T16:41:06Z Josh Chen 2021-04-17T16:41:06Z urn:sha1:092875d160a2d18c94bde41c6472e8031ab57313 start hprop stuff 2021-04-10T20:59:42Z Josh Chen 2021-04-10T20:59:42Z urn:sha1:d379e77dab3ff6a854b94af47be6098a2ba6ca64 rename things + some small changes 2021-01-31T02:54:51Z Josh Chen 2021-01-31T02:54:51Z urn:sha1:2feb56660700af107abb5a28a7120052ac405518 renamings 2021-01-21T00:52:13Z Josh Chen 2021-01-21T00:52:13Z urn:sha1:aff3d43d9865e7b8d082f0c239d2c73eee1fb291 Swapped notation for metas (now ?) and holes (now {}), other notation and name changes. 2021-01-18T23:49:13Z Josh Chen 2021-01-18T23:49:13Z urn:sha1:f46df86db9308dde29e0e5f97f54546ea1dc34bf Basic experiments adding reduction to the type checker 2020-09-23T15:03:42Z Josh Chen 2020-09-23T15:03:42Z urn:sha1:3922e24270518be67192ad6928bb839132c74c07