summaryrefslogtreecommitdiff
path: root/backends (unfollow)
Commit message (Expand)AuthorFilesLines
2023-06-19Add an example with even/odd in Diverge.leanSon Ho1-1/+119
2023-06-19Remove the obsolete examples from DivergeSon Ho1-208/+5
2023-06-19Simplify the id example in Diverge.leanSon Ho1-24/+95
2023-06-19Further simplify the proofs in Diverge.leanSon Ho1-122/+151
2023-06-19Make progress on making the proofs in Diverge more systematicSon Ho1-8/+252
2023-06-18Make minor modificationsSon Ho2-3/+3
2023-06-14Make minor modificationsSon Ho2-6/+26
2023-06-13Find sufficient validity criteria for Diverge.leanSon Ho1-41/+309
2023-06-09Start working on extrinsic proofs of terminationSon Ho4-7/+232
2023-06-09Reorganize a bit the Lean librarySon Ho4-22/+36
2023-06-06Remove the sorries from Primitives.leanSon Ho2-65/+120
2023-06-04Add a commentSon Ho1-3/+7
2023-06-04Update the HOL4 proofs for the last *release* version of HOL4Son Ho3-145/+137
2023-06-04Start setting up the Nix derivation for HOL4Son Ho2-1/+9
2023-06-04Simplify a proofSon Ho1-12/+6
2023-06-04Remove some obsolete files from the HOL4 backendSon Ho4-3302/+0
2023-06-04Finish the proofs of the hashmapSon Ho5-9/+98
2023-06-04Make progress on the proofs of the hash mapSon Ho5-2/+180
2023-06-04Make good progress on the proofs of the hashmap in HOL4Son Ho6-18/+155
2023-06-04Make the theorems used by the progress tactic persistentSon Ho8-186/+285
2023-06-04Commit saveThmsLib.sigSon Ho1-0/+46
2023-06-04Improve the parsing for divDefLibSon Ho1-1/+91
2023-06-04Fix some minor issuesSon Ho2-41/+49
2023-06-04Make progress on the HOL4 backendSon Ho2-42/+298
2023-06-04Make progress on extracting the HOL4 filesSon Ho2-2/+216
2023-06-04Make the unfolding theorems collection from evalLib persistentSon Ho9-242/+222
2023-06-04Make minor modificationsSon Ho1-5/+11
2023-06-04Start working on saveThmsLibSon Ho1-0/+190
2023-06-04Commit evalLibSon Ho2-0/+170
2023-06-04Update the definitions of mk_vec and vec_insert_backSon Ho2-21/+71
2023-06-04Cleanup a bit the HOL4 backend and implement eval_convSon Ho14-56/+238
2023-06-04Make good progress on generating code for HOL4Son Ho3-123/+736
2023-06-04Make a minor modificationSon Ho1-3/+5
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 09:32:08 +0000