feat: add Rewrite.Config.newGoals field

It is not used yet. We need a update-stage0.
leanprover · Jun 19, 2024 · dac1dac · dac1dac
1 parent d3a7569
commit dac1dac
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
@@ -1311,10 +1311,13 @@ structure ApplyConfig where
 
 namespace Rewrite
 
+abbrev NewGoals := ApplyNewGoals
+
 structure Config where
   transparency : TransparencyMode := .reducible
   offsetCnstrs : Bool := true
   occs : Occurrences := .all
+  newGoals : NewGoals := .nonDependentFirst
 
 end Rewrite