summaryrefslogtreecommitdiff
path: root/compiler/ExtractBuiltin.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-29had some fun writing an IsabelleHOL backendstuebinm1-9/+9
2024-06-05Add an option to run Aeneas as a borrow checkerSon Ho1-11/+13
2024-05-29Factor out code in ExtractBuiltin.mlSon Ho1-162/+122
2024-04-26Update compiler/ExtractBuiltin.mlSon HO1-1/+1
2024-04-25Update the backend and ExtractBuiltin.mlSon Ho1-1/+4
2024-04-24Add core::option::unwrap builtinZyad Hassan1-0/+2
2024-04-24compiler: introduce Lean-only translationsRyan Lahfa1-10/+25
2024-04-24compiler: map `core::option::Option::is_none` to `Option.isNone`Ryan Lahfa1-0/+4
2024-04-24compiler: map `core::mem::swap` to the pure swapRyan Lahfa1-0/+2
2024-04-17compiler: map `core::option::Option::take` to identity functionRyan Lahfa1-0/+4
2024-04-12Add more definitions to the Lean librarySon Ho1-0/+73
2024-04-12Start adding integer functions to the Lean librarySon Ho1-47/+142
2024-04-12Update the bindings for the extractionSon Ho1-14/+11
2024-04-03Add builtins for some checked ops such as checked_addZyad Hassan1-0/+31
2024-03-11Update a builtin nameSon Ho1-1/+1
2024-03-10Update the builtin name patternsSon Ho1-23/+66
2024-03-08Make progress on propagating the changesSon Ho1-6/+5
2024-03-08Remove the option to split fwd/back functions and update SymbolicToPureSon Ho1-87/+44
2023-12-22Update the library for F*Son Ho1-0/+8
2023-11-24Add the alloc::string::String type in the builtinsSon Ho1-3/+12
2023-11-22Make a minor modificationSon Ho1-2/+3
2023-11-22Use NameMatcher.NameMatcherMap instead of associative listsSon Ho1-5/+14
2023-11-21Reorganize the "Extract" filesSon Ho1-15/+10
2023-11-21Update more namesSon Ho1-6/+7
2023-11-21Fix issues with the builtin namesSon Ho1-48/+83
2023-11-20Fix minor issuesSon Ho1-3/+5
2023-11-20Fix minor issuesSon Ho1-2/+0
2023-11-20Use the name matcher implemented in CharonSon Ho1-260/+134
2023-11-15Start updating the name type, cleanup the names and the module abbrevsSon Ho1-3/+10
2023-11-09Make the traits work for CoqSon Ho1-1/+11
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-22 23:08:57 +0000