We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent c77d29f commit fb26a6bCopy full SHA for fb26a6b
Mathlib/Util/DelabNonCanonical.lean
@@ -47,3 +47,4 @@ def delabBinary (arity arg₁ arg₂ : Nat) (mkStx : Term → Term → DelabM Te
47
let (canonβ?, instDβ) ← withNaryArg arg₂ delabCheckingCanonical
48
-- fall through to normal delab if both canonical
49
if canonα? && canonβ? then failure
50
+ mkStx instDα instDβ
0 commit comments