| Commit message (Expand) | Author | Files | Lines |
2023-06-04 | Start setting up the Nix derivation for HOL4 | Son Ho | 2 | -5/+16 |
2023-06-04 | Add a comment | Son Ho | 1 | -1/+5 |
2023-06-04 | Finish the proofs of the hashmap | Son Ho | 2 | -463/+1461 |
2023-06-04 | Prove hash_map_insert_fwd_back_spec | Son Ho | 1 | -1/+59 |
2023-06-04 | Make progress on the proofs of the hash map | Son Ho | 1 | -4/+619 |
2023-06-04 | Make good progress on the proofs of the hashmap in HOL4 | Son Ho | 1 | -46/+686 |
2023-06-04 | Start working on the proofs of the hash map | Son Ho | 1 | -0/+543 |
2023-06-04 | Update tests/Makefile | Son Ho | 1 | -1/+1 |
2023-06-04 | Add the generated HOL4 files | Son Ho | 43 | -0/+13198 |
2023-06-04 | Make good progress on generating code for HOL4 | Son Ho | 11 | -109/+148 |
2023-06-04 | Add Result_Inhabited to Primitives.lean | Son Ho | 8 | -0/+24 |
2023-06-04 | Regenerate the translated files for Lean | Son Ho | 37 | -4931/+4452 |
2023-06-04 | Make a minor fix | Son Ho | 4 | -39/+32 |
2023-06-04 | Improve the generation of variant names for Lean | Son Ho | 11 | -451/+419 |
2023-06-04 | Improve simplify_aggregates to introduce structure updates | Son Ho | 7 | -314/+79 |
2023-06-04 | Start updating simplify_aggregates | Son Ho | 14 | -292/+589 |
2023-06-04 | Make minor modifications to the Lean files | Son Ho | 3 | -15/+14 |
2023-06-04 | Update the extraction of Lean files | Son Ho | 42 | -139/+364 |
2023-06-04 | Reorganize the Lean tests and extract the Polonius tests to Lean | Son Ho | 29 | -0/+2357 |
2023-06-04 | Remove the tests/lean/hashmap_on_disk/Main.lean file | Son Ho | 1 | -10/+0 |
2023-06-04 | Generate all the lakefile.lean files | Son Ho | 6 | -0/+108 |
2023-06-04 | Automate the generation of the lakefile.lean files | Son Ho | 1 | -7/+3 |
2023-06-04 | Update the generation of termination and decreases_by templates for Lean | Son Ho | 3 | -37/+37 |
2023-06-04 | Make minor modifications and regenerate the Lean files | Son Ho | 20 | -1488/+1599 |
2023-06-04 | WIP | Jonathan Protzenko | 2 | -233/+221 |
2023-06-04 | More comments | Jonathan Protzenko | 1 | -0/+8 |
2023-06-04 | Some prose | Jonathan Protzenko | 1 | -40/+45 |
2023-06-04 | Idiomatic naming conventions | Jonathan Protzenko | 5 | -271/+297 |
2023-06-04 | Improve formatting further by removing useless spaces | Son Ho | 5 | -90/+33 |
2023-06-04 | Make sure let-bindings in Lean end with line breaks and improve formatting | Son Ho | 23 | -334/+391 |
2023-06-04 | Improve formatting of the termination_by clauses | Son Ho | 3 | -84/+52 |
2023-06-04 | Make minor fixes, improve formatting for Lean and generate code for all the t... | Son Ho | 34 | -175/+5431 |
2023-06-04 | Make sure Main runs some code | Jonathan Protzenko | 1 | -2/+7 |
2023-06-04 | All of the generated code is syntactically correct | Jonathan Protzenko | 2 | -3/+3 |
2023-06-04 | WIP | Jonathan Protzenko | 6 | -40/+206 |
2023-06-04 | Fix runaway indentation | Jonathan Protzenko | 1 | -451/+440 |
2023-06-04 | Fill out more of the primitives file, attempt at type classes for scalar_cast | Jonathan Protzenko | 2 | -4/+28 |
2023-06-04 | Remove last sorry in Primitives | Jonathan Protzenko | 1 | -4/+2 |
2023-06-04 | Fill out Primitives.lean | Jonathan Protzenko | 2 | -10/+110 |
2023-06-04 | Don't need extra variables for the decreases clauses | Jonathan Protzenko | 1 | -11/+15 |
2023-06-04 | WIP printing proper clauses | Jonathan Protzenko | 1 | -35/+49 |
2023-06-04 | Fix some printing bits, proper syntax for terminates and decreases clauses | Jonathan Protzenko | 2 | -446/+481 |
2023-06-04 | WIP lots of stuff | Jonathan Protzenko | 4 | -24/+73 |
2023-06-04 | Fixup one primitive that is not assumed to be monadic | Jonathan Protzenko | 1 | -4/+4 |
2023-06-04 | Fix a syntax error | Jonathan Protzenko | 1 | -10/+5 |
2023-06-04 | Custom syntax support for structures in Lean | Jonathan Protzenko | 1 | -22/+71 |
2023-06-04 | More cosmetic improvements | Jonathan Protzenko | 2 | -89/+85 |
2023-06-04 | Fix a couple bugs here and there, improve Lean code-gen, still WIP | Jonathan Protzenko | 2 | -266/+310 |
2023-06-04 | New directory structure and corresponding extraction, + misc fixes, for Lean | Jonathan Protzenko | 8 | -132/+138 |
2023-06-04 | Write a tactic to discharge integer literal proof obligations | Jonathan Protzenko | 2 | -8/+27 |