Skip to content

Commit

Permalink
chore: add simp option unfoldPartialApp
Browse files Browse the repository at this point in the history
It is not being used yet, but we need to add it before solving issue #2042.
Reason: bootstrapping.
  • Loading branch information
leodemoura committed Oct 29, 2023
1 parent 08c47b2 commit 1abd5cc
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions src/Init/Meta.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1230,6 +1230,9 @@ structure Config where
/-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress. -/
failIfUnchanged : Bool := true
/-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded. -/
unfoldPartialApp : Bool := false
deriving Inhabited, BEq, Repr

end DSimp
Expand Down Expand Up @@ -1265,6 +1268,9 @@ structure Config where
it does not contain free or meta variables. Reduction is interrupted at a function application `f ...`
if `f` is marked to not be unfolded. -/
ground : Bool := false
/-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
will unfold even partial applications of `f` when we request `f` to be unfolded. -/
unfoldPartialApp : Bool := false
deriving Inhabited, BEq, Repr

-- Configuration object for `simp_all`
Expand Down

0 comments on commit 1abd5cc

Please sign in to comment.