We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
SlimCheck
1 parent 5561b43 commit c492cecCopy full SHA for c492cec
LSpec/SlimCheck/Checkable.lean
@@ -495,7 +495,7 @@ proposition where the quantifiers are annotated with `NamedBinder`.
495
scoped elab "mk_decorations" : tactic => do
496
let goalType ← (← getMainGoal).getType
497
if let Expr.app (.const ``Decorations.DecorationsOf ..) body := goalType then
498
- closeMainGoal `mk_decorations (addDecorations body)
+ closeMainGoal `SlimCheck.mk_decorations (addDecorations body)
499
500
end Decorations
501
0 commit comments