Lean4
@[tactic Mathlib.Tactic.subsingletonStx]
public meta def _aux_Mathlib_Tactic_Subsingleton___elabRules_Mathlib_Tactic_subsingletonStx_1 :
Lean.Elab.Tactic.Tactic✝ := fun
| `(tactic| subsingleton$[ [$[$instTerms?],*]]?) =>
withMainContext do
let recover := (← read).recover
let insts ← elabSubsingletonInsts instTerms?
Elab.Tactic.liftMetaTactic1 fun g => do
let (fvars, g) ← g.intros
try
g.subsingleton (insts := insts)
return none
catch e =>
-- Try `refl` when all else fails, to give a hint to the user
if recover then
try
g.refl <|> g.hrefl
let tac ←
if !fvars.isEmpty then
`(tactic| (intros; rfl))
else
`(tactic| rfl)
Meta.Tactic.TryThis.addSuggestion (← getRef) tac (origSpan? := ← getRef)
return none
catch _ =>
pure ()
throw e
| _ => no_error_if_unused% throwUnsupportedSyntax✝
