| Commit message (Expand) | Author | Files | Lines |
|---|
| 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 | 5 | -18/+36 |
| 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 | 23 | -129/+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 |
| 2023-06-04 | Add a sample test to illustrate potential project structure | Jonathan Protzenko | 9 | -0/+751 |
