Documentation

Lake.Util.Binder

@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
@[reducible, inline]
abbrev Lake.Hole :
Equations
Instances For
@[reducible, inline]
Equations
Equations
Equations
Equations
@[reducible, inline]
Equations
@[reducible, inline]
Equations
Instances For
instance Lake.instCoeBinderTSyntaxConsSyntaxNodeKindIdentKindMkStr4Nil :
Coe Binder (Lean.TSyntax [Lean.identKind, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder])
Equations
@[reducible, inline]
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.