summaryrefslogtreecommitdiff
path: root/backends (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-04Introduce fix_exec, an executable version of fixSon Ho5-13/+90
2023-06-04Make minor modificationsSon Ho2-8/+35
2023-06-04Make minor modifications to divDefLibSon Ho2-60/+65
2023-06-04Fix minor issuesSon Ho3-12/+508
2023-06-04Fix minor issuesSon Ho2-6/+17
2023-06-04Do more cleanupSon Ho2-1222/+0
2023-06-04Cleanup the files of the HOL4 backendSon Ho16-3080/+2938
2023-06-04Reimplement DefineDiv with the new fixed point operatorSon Ho3-2/+1249
2023-06-04Write some tests for divDefProto2Script.smlSon Ho2-84/+214
2023-06-04Update divDefProto2Script.smlSon Ho1-55/+16
2023-06-04Write a prototype definition using the general fixed-point combinatorSon Ho2-510/+417
2023-06-04Start working on more general fixed-point combinatorsSon Ho3-0/+904
2023-06-04Cleanup divDefProtoScriptSon Ho2-523/+12
2023-06-04Improve the performance of dependent rewrites by using netsSon Ho2-58/+120
2023-06-04Make more proofs about the hashmap protoSon Ho5-4/+225
2023-06-04Update the hashmap proofs and fix some tacticsSon Ho5-46/+300
2023-06-04Start working on a version of divDefLib which uses fixed point combinatorsSon Ho2-0/+983
2023-06-04Cleanup a bit and reorganizeSon Ho6-90/+577
2023-06-04Make minor modificationsSon Ho1-0/+26
2023-06-04Fix minor bugs in divDefLib.smlSon Ho1-28/+134
2023-06-04Fix a small issueSon Ho1-3/+32
2023-06-04Cleanup a bitSon Ho1-220/+136
2023-06-04Finish a first working version of divDefLib.smlSon Ho1-29/+347
2023-06-04Start working on divDefLib for diverging definitionsSon Ho9-111/+995
2023-06-04Add a .sig fileSon Ho1-0/+202
2023-06-04Reorganize the HOL4 files and fix some issues with the arithmetic proofsSon Ho4-763/+568
2023-06-04Make progress on the standard library for HOL4Son Ho9-91/+1041
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 10:24:22 +0000