_aux_Mathlib_Tactic_Peel___elabRules_Mathlib_Tactic_Peel_peel_1

Lean4
@[tactic Mathlib.Tactic.Peel.peel]
public meta def _aux_Mathlib_Tactic_Peel___elabRules_Mathlib_Tactic_Peel_peel_1 : Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| peel$[$num?:num]? $e:term$[ with $l?* $n?]?) =>
    withMainContext do
      /- we use `elabTermForApply` instead of `elabTerm` so that terms passed to `peel` can contain
          quantifiers with implicit bound variables without causing errors or requiring `@`. -/

      let e ← elabTermForApply e false
      let n? := n?.bind fun n => if n.raw.isIdent then pure n.raw.getId else none
      let l := (l?.getD #[]).map getNameOfIdent' |>.toList
      let num? := num?.map (·.getNat) <|> if l.isEmpty then none else l.length
      if let some num := num? then
        peelArgs e num l n?
      else
        unless ← peelUnbounded e n? do
          throwPeelError (← inferType e) (← getMainTarget)
  | `(tactic| peel$n:num) => peelArgsIff <| .replicate n.getNat `_
  | `(tactic| peel with $args*) => peelArgsIff (args.map getNameOfIdent').toList
  | _ => no_error_if_unused% throwUnsupportedSyntax✝
Похожие утверждения