diff options
| author | Ryan Lahfa | 2024-04-24 10:47:26 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-04-24 11:10:35 +0200 |
| commit | 5f2a388d1ff039cde0d78daaba58c191b404405e (patch) | |
| tree | cff8db0f0a0210be73db5320bde6f385381ffb45 /backends/hol4 | |
| parent | 8b1fd2477148d5c7174b5175074d480b1cb2cf06 (diff) | |
compiler: introduce Lean-only translations
On the long run, all backends will not have equivalent or equal support
for extraction.
This introduces a function to filter out some Lean-only definitions in
our various arrays of core functions.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions