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

chore: parseQuotWithCurrentStage and quotPrecheck

Browse source
This commit is contained in:
Sebastian Ullrich 2022-11-04 10:55:56 +01:00
parent 140d10819d
commit f5c13f9db8
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/stdlib_flags.h
View file

@ -9,6 +9,10 @@ options get_default_options() {
opts = opts.update({"interpreter", "prefer_native"}, false);
// switch to `true` for changing built-in parsers used in quotations
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
// toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
// with custom precheck hooks were affected
opts = opts.update({"quotPrecheck"}, true);
opts = opts.update({"pp", "rawOnError"}, true);
#endif
return opts;