We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent dc7ff37 commit 81a1319Copy full SHA for 81a1319
Mathlib/Util/DelabNonCanonical.lean
@@ -16,6 +16,7 @@ Synthesized instances are considered 'canonical' for this purpose.
16
-/
17
18
public meta section
19
+open Lean Meta PrettyPrinter.Delaborator SubExpr
20
21
/-- When the delab reader is pointed at an expression for an instance, returns `(true, t)`
22
**iff** instance synthesis succeeds and produces a defeq instance; otherwise returns `(false, t)`.
0 commit comments