update dsimp

Author: kmill

src/Init/MetaTypes.lean

@@ -57,8 +57,9 @@ It is immediately converted to `Lean.Meta.Simp.Config` by `Lean.Elab.Tactic.elab
 -/
 structure Config where
   /--
-  When `true` (default: `true`), performs zeta reduction of let expressions.
+  When `true` (default: `true`), performs zeta reduction of `let` and `have` expressions.
   That is, `let x := v; e[x]` reduces to `e[v]`.
+  If `zetaHave` is `false` then `have` expressions are not zeta reduced.
   See also `zetaDelta`.
   -/
   zeta              : Bool := true
@@ -107,7 +108,8 @@ structure Config where
   unfoldPartialApp  : Bool := false
   /--
   When `true` (default: `false`), local definitions are unfolded.
-  That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
+  That is, given a local context containing `x : t := e`, then the free variable `x` reduces to `e`.
+  Otherwise, `x` must be provided as a `simp` argument.
   -/
   zetaDelta         : Bool := false
   /--
@@ -116,10 +118,17 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  When `true` (default : `true`), then simps will remove unused let-declarations:
+  When `true` (default : `true`), then `simp` will remove unused `let` and `have` expressions:
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   -/
   zetaUnused : Bool := true
+  /--
+  (Unimplemented)
+  When `false` (default: `true`), then disables zeta reduction of `have` expressions.
+  If `zeta` is `false`, then this option has no effect.
+  Unused `have`s are still removed if `zeta` or `zetaUnused` are true.
+  -/
+  zetaHave : Bool := true
   deriving Inhabited, BEq
 
 end DSimp