summaryrefslogtreecommitdiff
path: root/backends (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Cleanup a bitSon Ho3-191/+17
2023-06-04Make progress on primitivesScriptSon Ho6-211/+333
2023-06-04Make more progress on primitivesScript.smlSon Ho2-209/+191
2023-06-04Use lower case in the names for the HOL4 backendSon Ho5-832/+771
2023-06-04Make progress on primitivesScript.sml and experiment a bitSon Ho4-87/+890
2023-06-04Make progress on the primitives library for HOL4Son Ho3-12/+196
2023-06-04Organize a bit the HOL filesSon Ho8-190/+1160
2023-06-04Make minor modificationsSon Ho1-5/+0
2023-06-04Add a HolmakefileSon Ho5-17/+2527
2023-06-04Make good progress on Primitives.smlSon Ho1-24/+997
2023-06-04Start working on Primitives.smlSon Ho2-5/+387
2023-06-04Add a more interesting exampleSon Ho1-1/+69
2023-06-04Implement a progress tacticSon Ho1-33/+339
2023-06-04Make more progress on the automationSon Ho1-51/+199
2023-06-04Make minor modifications to the HOL experimentSon Ho1-5/+25
2023-06-04Make progress on implementing tacticsSon Ho1-27/+347
2023-06-04Implement [assume_bounds_for_all_int_vars] to improve the proof experienceSon Ho1-80/+145
2023-06-04Start making tests in HOL4Son Ho1-0/+825
2023-06-04Add Result_Inhabited to Primitives.leanSon Ho1-0/+3
2023-06-04Make more updates for the Lean backendSon Ho1-33/+57
2023-06-04Update Primitives.leanSon Ho1-90/+58
2023-06-04Update Primitives.leanSon Ho1-194/+390
2023-06-04Add backends/lean/lakefile.leanSon Ho3-0/+39
2023-06-04Make minor modifications and regenerate the Lean filesSon Ho1-1/+1
2023-06-04WIPJonathan Protzenko1-35/+41
2023-06-04More commentsJonathan Protzenko1-40/+53
2023-06-04Idiomatic naming conventionsJonathan Protzenko1-46/+46
2023-06-04Rename primitives.lean to Primitives.leanSon Ho1-0/+0
2023-06-04WIPJonathan Protzenko1-26/+50
2023-06-04Fill out more of the primitives file, attempt at type classes for scalar_castJonathan Protzenko1-2/+26
2023-06-04Remove last sorry in PrimitivesJonathan Protzenko1-10/+105
2023-06-04Fix some printing bits, proper syntax for terminates and decreases clausesJonathan Protzenko1-3/+30
2023-06-04WIP lots of stuffJonathan Protzenko1-5/+30
2023-06-04Fixup one primitive that is not assumed to be monadicJonathan Protzenko1-4/+4
2023-06-04More cosmetic improvementsJonathan Protzenko1-0/+1
2023-06-04Fix a couple bugs here and there, improve Lean code-gen, still WIPJonathan Protzenko1-0/+1
2023-06-04New directory structure and corresponding extraction, + misc fixes, for LeanJonathan Protzenko1-7/+9
2023-06-04Write a tactic to discharge integer literal proof obligationsJonathan Protzenko1-4/+23
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-0/+155
2023-02-03Do not unfold the monadic lets for the generated F* codeSon Ho1-1/+3
2022-11-16Make minor modifications to the extractionSon Ho2-12/+14
2022-11-14Add a `-use-fuel` optionSon Ho1-0/+3
2022-11-14Make [Result::Failure] type an [Error] parameterSon Ho3-33/+88
2022-11-14Make good progress on the Coq backendSon Ho1-0/+478
2022-11-11Move the fstar files to the new backends directorySon Ho1-0/+287
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 16:50:52 +0000