lean4-htt/stage0
Sebastian Ullrich fb23d7b45d
chore: make parseQuotWithCurrentStage do what it says under prefer_native (#10058)
Switch on the interpreter when entering quotations under this option
2025-08-22 15:14:43 +00:00
..
src chore: make parseQuotWithCurrentStage do what it says under prefer_native (#10058) 2025-08-22 15:14:43 +00:00
stdlib chore: update stage0 2025-08-22 14:07:57 +00:00