d9bc9ee | Josh Chen | 30 November 2022, 12:22:20 UTC | update readme | 30 November 2022, 12:22:20 UTC |
5655750 | Josh Chen | 28 June 2021, 15:06:19 UTC | 1. Thm/def statement display. 2. Syntax + computation proof. | 28 June 2021, 15:06:19 UTC |
06f38e1 | Josh Chen | 28 June 2021, 12:34:31 UTC | begin refactoring Equivalence | 28 June 2021, 12:34:31 UTC |
f988d54 | Josh Chen | 24 June 2021, 21:40:05 UTC | Bad practice huge commit: 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file | 24 June 2021, 21:40:05 UTC |
0085798 | Josh Chen | 23 June 2021, 15:26:23 UTC | 1. Put universe level parameters first in automatic term definitions. 2. Add debugging to typechecker | 23 June 2021, 15:26:23 UTC |
1928649 | Josh Chen | 17 April 2021, 16:55:04 UTC | update readme | 17 April 2021, 16:55:04 UTC |
eab890b | Josh Chen | 17 April 2021, 16:53:48 UTC | update CI to Isabelle 2021 | 17 April 2021, 16:53:48 UTC |
75ab44c | Josh Chen | 17 April 2021, 16:41:56 UTC | Merge branch 'dev' | 17 April 2021, 16:41:56 UTC |
092875d | Josh Chen | 17 April 2021, 16:41:06 UTC | Patch proof. Now works on Isabelle2021. | 17 April 2021, 16:41:06 UTC |
3a34ca2 | Josh Chen | 17 April 2021, 16:16:45 UTC | Small fix: extraneous variable | 17 April 2021, 16:16:45 UTC |
54df733 | Josh Chen | 10 April 2021, 21:06:24 UTC | small rename | 10 April 2021, 21:06:24 UTC |
af3b0cc | Josh Chen | 10 April 2021, 21:06:04 UTC | update Isabelle2020 URL in Dockerfile | 10 April 2021, 21:06:04 UTC |
d379e77 | Josh Chen | 10 April 2021, 20:59:42 UTC | start hprop stuff | 10 April 2021, 20:59:42 UTC |
2570ac5 | Josh Chen | 01 February 2021, 13:03:19 UTC | update readme | 01 February 2021, 13:03:19 UTC |
2feb566 | Josh Chen | 31 January 2021, 02:54:51 UTC | rename things + some small changes | 31 January 2021, 02:54:51 UTC |
aff3d43 | Josh Chen | 21 January 2021, 00:52:13 UTC | renamings | 21 January 2021, 00:52:13 UTC |
6d8fa47 | Josh Chen | 19 January 2021, 02:44:03 UTC | Forgot to update ROOT | 19 January 2021, 02:44:03 UTC |
549f1d4 | Josh Chen | 19 January 2021, 02:18:44 UTC | Bugfix: no longer repeatedly add duplicate rules to simpset | 19 January 2021, 02:18:44 UTC |
f46df86 | Josh Chen | 18 January 2021, 23:49:13 UTC | Swapped notation for metas (now ?) and holes (now {}), other notation and name changes. | 18 January 2021, 23:49:13 UTC |
3922e24 | Josh Chen | 23 September 2020, 15:03:42 UTC | Basic experiments adding reduction to the type checker | 23 September 2020, 15:03:42 UTC |
77df99b | Josh Chen | 14 August 2020, 17:55:38 UTC | minor | 14 August 2020, 17:55:38 UTC |
d172f9d | Josh Chen | 14 August 2020, 09:21:59 UTC | reorganize | 14 August 2020, 09:21:59 UTC |
7a53528 | Josh Chen | 14 August 2020, 09:11:34 UTC | update license file list | 14 August 2020, 09:11:34 UTC |
bd2efac | Josh Chen | 14 August 2020, 09:07:17 UTC | (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. | 14 August 2020, 09:07:17 UTC |
8f4ff41 | Josh Chen | 09 August 2020, 16:34:58 UTC | (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 | 09 August 2020, 16:34:58 UTC |
c530305 | Josh Chen | 05 August 2020, 13:21:43 UTC | 1. fix intros method. 2. Couple extra lemmas; good small test cases for normalization in typechecking/elaboration. | 05 August 2020, 13:21:43 UTC |
710f314 | Josh Chen | 03 August 2020, 11:34:53 UTC | (FEAT) SIDE_CONDS tactical has additional argument specifying how many initial subgoals to skip applying the side condition solver to. (FEAT) `intro`, `intros` methods for "logical introduction rules" (as opposed to typechecking `intr` attribute), only works on conclusions with rigid type. (FEAT) CREPEAT_N bounded repetition tactical, used in `intros n` method. | 03 August 2020, 11:34:53 UTC |
70fd3f7 | Josh Chen | 02 August 2020, 14:44:47 UTC | rename some theorems | 02 August 2020, 14:44:47 UTC |
77aa107 | Josh Chen | 31 July 2020, 16:10:10 UTC | (REF) Tweak attribute names in preparation for new logical introduction rule behavior | 31 July 2020, 16:10:10 UTC |
ff54548 | Josh Chen | 31 July 2020, 12:56:24 UTC | (FEAT) Term elaboration of assumption and goal statements. . 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. | 31 July 2020, 12:56:24 UTC |
2b0e14b | Josh Chen | 28 July 2020, 12:24:22 UTC | small improvement | 28 July 2020, 12:24:22 UTC |
6b27aa5 | Josh Chen | 28 July 2020, 12:10:34 UTC | New `assuming` proof command for elaborated assumptions | 28 July 2020, 12:10:34 UTC |
223a253 | Josh Chen | 27 July 2020, 12:31:35 UTC | Merge branch 'dev' | 27 July 2020, 12:31:35 UTC |
2a78ddc | Josh Chen | 27 July 2020, 12:31:09 UTC | update .gitignore | 27 July 2020, 12:31:09 UTC |
0f84aa0 | Josh Chen | 27 July 2020, 12:29:48 UTC | Hook elaboration into assumptions mechanism | 27 July 2020, 12:29:48 UTC |
f20d91f | Josh Chen | 23 July 2020, 11:00:04 UTC | minor | 23 July 2020, 11:00:04 UTC |
184b1d4 | Josh Chen | 22 July 2020, 13:48:33 UTC | remove theory | 22 July 2020, 13:48:33 UTC |
4be339f | Josh Chen | 22 July 2020, 13:30:27 UTC | begin work on pre-proof elaboration | 22 July 2020, 13:30:27 UTC |
6464ab5 | Josh Chen | 21 July 2020, 17:31:31 UTC | minor | 21 July 2020, 17:31:31 UTC |
3067216 | Josh Chen | 21 July 2020, 14:28:05 UTC | 1. Bugfix: implicits now properly name schematic variables. Fixes problems caused by variable name clashes. 2. reduce method now more principled: restricts to repeating on first subgoal. 3. An example declarative proof in Equivalence.thy. | 21 July 2020, 14:28:05 UTC |
dfd241b | Josh Chen | 21 July 2020, 00:16:14 UTC | Merge pull request #8 from jaycech3n/dev Merge big diff on dev | 21 July 2020, 00:16:14 UTC |
12eed86 | Josh Chen | 21 July 2020, 00:09:44 UTC | 1. Type-checking/inference now more principled, and the implementation is better. 2. Changed most tactics to context tactics. | 21 July 2020, 00:09:44 UTC |
6aaf4d5 | Josh Chen | 17 July 2020, 11:48:30 UTC | link | 17 July 2020, 11:48:30 UTC |
1130633 | Josh Chen | 17 July 2020, 09:30:34 UTC | add build status | 17 July 2020, 09:30:34 UTC |
de4d802 | Josh Chen | 17 July 2020, 09:27:42 UTC | rename action | 17 July 2020, 09:27:42 UTC |
b7439e6 | Josh Chen | 17 July 2020, 09:15:26 UTC | Merge pull request #7 from jaycech3n/ci-action Ci action | 17 July 2020, 09:15:26 UTC |
00463d7 | Josh Chen | 17 July 2020, 09:12:00 UTC | looks like descriptions not allowed in workflow job yaml | 17 July 2020, 09:12:00 UTC |
9eb4aeb | Josh Chen | 17 July 2020, 09:11:13 UTC | final test push | 17 July 2020, 09:11:13 UTC |
f510ca7 | Josh Chen | 17 July 2020, 09:06:19 UTC | fix path | 17 July 2020, 09:06:19 UTC |
877b951 | Josh Chen | 17 July 2020, 09:03:22 UTC | test | 17 July 2020, 09:03:22 UTC |
66b180a | Josh Chen | 17 July 2020, 08:51:26 UTC | check home var | 17 July 2020, 08:51:26 UTC |
6e54cf5 | Josh Chen | 17 July 2020, 08:47:20 UTC | change HOME env var, more testing... | 17 July 2020, 08:47:20 UTC |
1ff98c9 | Josh Chen | 17 July 2020, 08:41:19 UTC | more test | 17 July 2020, 08:41:19 UTC |
31dca57 | Josh Chen | 17 July 2020, 08:35:07 UTC | more testing | 17 July 2020, 08:35:07 UTC |
e75a2a2 | Josh Chen | 16 July 2020, 21:31:04 UTC | probe directories | 16 July 2020, 21:31:04 UTC |
6f2dc47 | Josh Chen | 16 July 2020, 21:28:28 UTC | test | 16 July 2020, 21:28:28 UTC |
61f2b77 | Josh Chen | 16 July 2020, 21:24:34 UTC | try try again | 16 July 2020, 21:24:34 UTC |
64a41c3 | Josh Chen | 16 July 2020, 17:53:11 UTC | try again | 16 July 2020, 17:53:11 UTC |
1f98940 | Josh Chen | 16 July 2020, 17:33:51 UTC | I think I figured out the problem | 16 July 2020, 17:33:51 UTC |
f2614cb | Josh Chen | 16 July 2020, 17:31:55 UTC | try ADD instead of RUN curl | 16 July 2020, 17:31:55 UTC |
a31c2a9 | Josh Chen | 16 July 2020, 17:25:46 UTC | will this parse now? | 16 July 2020, 17:25:46 UTC |
ddb5325 | Josh Chen | 16 July 2020, 17:22:32 UTC | fix | 16 July 2020, 17:22:32 UTC |
402a802 | Josh Chen | 16 July 2020, 17:19:03 UTC | download Isabelle from TUM archives | 16 July 2020, 17:19:03 UTC |
d81a1db | Josh Chen | 16 July 2020, 16:59:34 UTC | fix action path | 16 July 2020, 16:59:34 UTC |
f822581 | Josh Chen | 16 July 2020, 16:57:13 UTC | set up CI | 16 July 2020, 16:57:13 UTC |
3bcaf5d | Josh Chen | 16 July 2020, 14:46:09 UTC | Checkpoint. THIS BUILD WILL FAIL | 16 July 2020, 14:46:09 UTC |
2a2fa1e | Josh Chen | 16 July 2020, 14:20:15 UTC | update readme | 16 July 2020, 14:20:15 UTC |
79659cb | Josh Chen | 11 July 2020, 13:13:20 UTC | Defined annotated terms to be used in future typechecking improvements | 11 July 2020, 13:13:20 UTC |
7d59cf1 | Josh Chen | 11 July 2020, 13:11:37 UTC | fix file location reference in license | 11 July 2020, 13:11:44 UTC |
8612748 | Josh Chen | 11 July 2020, 13:10:42 UTC | rename file | 11 July 2020, 13:10:42 UTC |
831f334 | Josh Chen | 09 July 2020, 11:35:39 UTC | Non-annotated object lambda | 09 July 2020, 11:35:39 UTC |
fc9ba21 | Josh Chen | 09 July 2020, 10:58:13 UTC | caveat | 09 July 2020, 10:58:13 UTC |
07c51b1 | Josh Chen | 08 July 2020, 13:55:48 UTC | 1. Initial `Definition` keyword. 2. ifelse. | 08 July 2020, 13:55:48 UTC |
f0fab6e | Josh Chen | 08 July 2020, 13:54:04 UTC | minor | 08 July 2020, 13:54:04 UTC |
4f147cb | Josh Chen | 19 June 2020, 10:41:54 UTC | reorganize | 19 June 2020, 10:41:54 UTC |
8885f9c | Josh Chen | 15 June 2020, 09:58:30 UTC | fix ROOT | 15 June 2020, 09:58:30 UTC |
28e91f9 | Josh Chen | 15 June 2020, 09:56:28 UTC | remove old folder | 15 June 2020, 09:56:28 UTC |
e42b7b3 | Josh Chen | 15 June 2020, 09:53:44 UTC | Merge branch 'dev' | 15 June 2020, 09:53:44 UTC |
69bf074 | Josh Chen | 15 June 2020, 09:52:19 UTC | rename folders | 15 June 2020, 09:52:19 UTC |
8d6d633 | Josh Chen | 04 June 2020, 12:27:41 UTC | some documentation | 04 June 2020, 12:27:41 UTC |
9050b74 | Josh Chen | 03 June 2020, 11:10:35 UTC | Merge branch 'dev' | 03 June 2020, 11:10:35 UTC |
515c142 | Josh Chen | 03 June 2020, 11:09:45 UTC | rule name | 03 June 2020, 11:09:45 UTC |
e513fc2 | Josh Chen | 03 June 2020, 11:09:30 UTC | 1. Type information context data 2. Small reformulations of rules 3. Bool | 03 June 2020, 11:09:30 UTC |
ccc26cf | Josh Chen | 01 June 2020, 15:33:40 UTC | update | 01 June 2020, 15:33:47 UTC |
8c0205a | Josh Chen | 01 June 2020, 15:26:39 UTC | update | 01 June 2020, 15:26:39 UTC |
cf5136f | Josh Chen | 01 June 2020, 15:22:09 UTC | update | 01 June 2020, 15:22:09 UTC |
29112d6 | Josh Chen | 01 June 2020, 15:19:27 UTC | reorganize and add some material | 01 June 2020, 15:19:27 UTC |
0834e99 | Josh Chen | 01 June 2020, 15:18:39 UTC | readme | 01 June 2020, 15:18:39 UTC |
dc3800f | Josh Chen | 31 May 2020, 11:14:35 UTC | more list | 31 May 2020, 11:14:35 UTC |
c3606c3 | Josh Chen | 30 May 2020, 23:13:42 UTC | multiplication | 30 May 2020, 23:13:42 UTC |
4faad4f | Josh Chen | 30 May 2020, 23:13:34 UTC | transport method | 30 May 2020, 23:13:34 UTC |
1263127 | Josh Chen | 30 May 2020, 16:29:46 UTC | add and mul recurse on second argument instead of first | 30 May 2020, 16:29:46 UTC |
68bbcdc | Josh Chen | 30 May 2020, 16:29:11 UTC | inhabitation coercion should be syntax, not logical constant! | 30 May 2020, 16:29:11 UTC |
2e807b7 | Josh Chen | 30 May 2020, 12:38:12 UTC | fix name | 30 May 2020, 12:38:12 UTC |
9ed05b8 | Josh Chen | 29 May 2020, 17:59:22 UTC | proved a few oopses + minor tweaks | 29 May 2020, 17:59:22 UTC |
02cfe2a | Josh Chen | 29 May 2020, 17:58:29 UTC | fix Pi congruence rule | 29 May 2020, 17:58:29 UTC |
484988b | Josh Chen | 29 May 2020, 12:28:17 UTC | todo list | 29 May 2020, 12:28:17 UTC |
2f4e9b9 | Josh Chen | 29 May 2020, 08:37:46 UTC | clean up Eckmann-Hilton and move to Identity | 29 May 2020, 08:37:46 UTC |
41da54e | Josh Chen | 29 May 2020, 08:20:36 UTC | minor | 29 May 2020, 08:20:36 UTC |
417af1a | Josh Chen | 28 May 2020, 14:00:42 UTC | bit more material | 28 May 2020, 14:00:42 UTC |