max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: split Init.Meta in preparation for meta semantics restrictions (#10343)

Browse source
This commit is contained in:
Sebastian Ullrich 2025-09-11 15:01:03 +02:00 • committed by GitHub
parent 5c06c79c15
commit 73c85b177e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 1685 additions and 1672 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1674
src/Init/Meta.lean
View file

File diff suppressed because it is too large Load diff

1679
src/Init/Meta/Defs.lean Normal file
View file

File diff suppressed because it is too large Load diff

4
stage0/src/stdlib_flags.h
View file

@ -11,12 +11,12 @@ options get_default_options() {
opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
// switch to `true` for ABI-breaking changes affecting meta code;
// see also next option!
opts = opts.update({"interpreter", "prefer_native"}, false);
opts = opts.update({"interpreter", "prefer_native"}, true);
// switch to `false` when enabling `prefer_native` should also affect use
// of built-in parsers in quotations; this is usually the case, but setting
// both to `true` may be necessary for handling non-builtin parsers with
// builtin elaborators
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
// changes to builtin parsers may also require toggling the following option if macros/syntax
// with custom precheck hooks were affected
opts = opts.update({"quotPrecheck"}, true);