Documentation

MRiscX.Elab.CodeElaborator

source
def getInstrExpr (t : Lean.TSyntax `mriscx_Instr) :
Lean.Elab.TermElabM Lean.Expr
Equations
    Instances For
      source
      def getInstructionExprArr (seq : Lean.TSyntaxArray `mriscx_Instr) :
      Lean.Elab.TermElabM (Array Lean.Expr)
      Equations
        Instances For
          source
          def getLabelInstrArr (t : Lean.TSyntax `mriscx_label) :
          Lean.Elab.TermElabM (String × Array Lean.Expr)
          Equations
            Instances For
              source
              def getLabelMapFromSyntax (syn : Lean.TSyntax `mriscx_syntax) :
              Lean.Elab.TermElabM LabelMap
              Equations
                Instances For
                  source
                  def getCodeFromSyntax (syn : Lean.TSyntax `mriscx_syntax) :
                  Lean.Elab.TermElabM Lean.Expr
                  Equations
                    Instances For
                      source
                      def term__1 :
                      Lean.ParserDescr
                      Equations
                        Instances For
                          source
                          def term__2 :
                          Lean.ParserDescr
                          Equations
                            Instances For