summaryrefslogtreecommitdiff
path: root/compiler/ExtractBuiltin.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-10-26Make minor modifications and update the array test for F*Son Ho1-1/+4
2023-10-26Fix some issues and regenerate the HashmapMain example for LeanSon Ho1-1/+10
2023-10-26Improve the handling of saved function effects in ExtractBuiltin.mlSon Ho1-13/+27
2023-10-26Make progress on fixing the extractionSon Ho1-8/+24
2023-10-26Improve ExtractBuiltin.mlSon Ho1-37/+49
2023-10-26Fix more issues at extraction and factor out defs in ExtractBuiltinSon Ho1-260/+143
2023-10-25Make the hashmap files typecheck again in LeanSon Ho1-347/+162
2023-10-25Fix some issues at extraction and add builtinsSon Ho1-5/+299
2023-10-24Handle properly the builtin, non fallible functionsSon Ho1-1/+33
2023-10-24Start taking into account non-fallible functions like core::mem::replaceSon Ho1-0/+8
2023-10-24Fix minor issuesSon Ho1-4/+4
2023-10-24Filter some type arguments for the builtin types/functionsSon Ho1-8/+7
2023-10-24Add support for builtin trait implementationsSon Ho1-0/+34
2023-10-24Fix various issues with the builtinsSon Ho1-20/+62
2023-10-23Make progress on handling the builtinsSon Ho1-42/+51
2023-10-23Remove some assumed types and add more support for builtin definitionsSon Ho1-0/+468
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 01:51:35 +0000