Un-exit source (stage0 audit)

instead of c1c13d2

Author: kim-em

src/Lean/Elab/Tactic/HaveI.lean

@@ -13,47 +13,3 @@ but instead inline the value instead.
 This is useful to declare local instances and proofs in theorem statements
 and subgoals, where the extra binding is inconvenient.
 -/
-
-#exit
-
-namespace Std.Tactic
-
-
-macro_rules
-  | `(haveI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
-    `(haveI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
-  | `(haveI _ $bs* := $val; $body) => `(haveI x $bs* : _ := $val; $body)
-  | `(haveI _ $bs* : $ty := $val; $body) => `(haveI x $bs* : $ty := $val; $body)
-  | `(haveI $x:ident $bs* := $val; $body) => `(haveI $x $bs* : _ := $val; $body)
-  | `(haveI $_:ident $_* : $_ := $_; $_) => throwUnsupported -- handled by elab
-
-macro_rules
-  | `(letI $hy:hygieneInfo $bs* $[: $ty]? := $val; $body) =>
-    `(letI $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $ty]? := $val; $body)
-  | `(letI _ $bs* := $val; $body) => `(letI x $bs* : _ := $val; $body)
-  | `(letI _ $bs* : $ty := $val; $body) => `(letI x $bs* : $ty := $val; $body)
-  | `(letI $x:ident $bs* := $val; $body) => `(letI $x $bs* : _ := $val; $body)
-  | `(letI $_:ident $_* : $_ := $_; $_) => throwUnsupported -- handled by elab
-
-elab_rules <= expectedType
-  | `(haveI $x:ident $bs* : $ty := $val; $body) => do
-    let (ty, val) ← elabBinders bs fun bs => do
-      let ty ← elabType ty
-      let val ← elabTermEnsuringType val ty
-      pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
-    withLocalDeclD x.getId ty fun x => do
-      return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
-
-elab_rules <= expectedType
-  | `(letI $x:ident $bs* : $ty := $val; $body) => do
-    let (ty, val) ← elabBinders bs fun bs => do
-      let ty ← elabType ty
-      let val ← elabTermEnsuringType val ty
-      pure (← mkForallFVars bs ty, ← mkLambdaFVars bs val)
-    withLetDecl x.getId ty val fun x => do
-      return (← (← elabTerm body expectedType).abstractM #[x]).instantiate #[val]
-
-/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
-macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_)
-/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
-macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)