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