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 leanprover#2042.
Reason: bootstrapping.
  • Loading branch information
leodemoura authored and Komyyy committed Nov 2, 2023
1 parent 19e7c0a commit dc1cb69
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 dc1cb69

Please sign in to comment.