Documentation

Qq.Match

Instances For
    Instances For
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            def Qq.Impl.mkLetDoSeqItem {m : TypeType} [Monad m] [Lean.MonadQuotation m] (pat : Lean.Term) (rhs : Lean.TSyntax `doElem) (alt : Lean.TSyntax `Lean.Parser.Term.doSeq) :
            m (List (Lean.TSyntax `Lean.Parser.Term.doSeqItem))
            Instances For
              partial def Qq.Impl.floatQMatch (alt : Lean.TSyntax `Lean.Parser.Term.doSeq) :
              Lean.TermStateT (List (Lean.TSyntax `Lean.Parser.Term.doSeqItem)) Lean.MacroM Lean.Term