Documentation

Lean.Compiler.IR.Checker

source
@[extern lean_get_max_ctor_fields]
opaque Lean.IR.Checker.getMaxCtorFields :
Unit → Nat
source
def Lean.IR.Checker.maxCtorFields :
Nat
Equations
    Instances For
      source
      @[extern lean_get_max_ctor_scalars_size]
      opaque Lean.IR.Checker.getMaxCtorScalarsSize :
      Unit → Nat
      source
      def Lean.IR.Checker.maxCtorScalarsSize :
      Nat
      Equations
        Instances For
          source
          @[extern lean_get_max_ctor_tag]
          opaque Lean.IR.Checker.getMaxCtorTag :
          Unit → Nat
          source
          def Lean.IR.Checker.maxCtorTag :
          Nat
          Equations
            Instances For
              source
              @[extern lean_get_usize_size]
              opaque Lean.IR.Checker.getUSizeSize :
              Unit → Nat
              source
              def Lean.IR.Checker.usizeSize :
              Nat
              Equations
                Instances For
                  source
                  structure Lean.IR.Checker.CheckerContext :
                  Type
                  Instances For
                    source
                    structure Lean.IR.Checker.CheckerState :
                    Type
                    Instances For
                      source
                      @[reducible, inline]
                      abbrev Lean.IR.Checker.M (α : Type) :
                      Type
                      Equations
                        Instances For
                          source
                          def Lean.IR.Checker.markIndex (i : Index) :
                          M Unit
                          Equations
                            Instances For
                              source
                              def Lean.IR.Checker.markVar (x : VarId) :
                              M Unit
                              Equations
                                Instances For
                                  source
                                  def Lean.IR.Checker.markJP (j : JoinPointId) :
                                  M Unit
                                  Equations
                                    Instances For
                                      source
                                      def Lean.IR.Checker.getDecl (c : Name) :
                                      M Decl
                                      Equations
                                        Instances For
                                          source
                                          def Lean.IR.Checker.checkVar (x : VarId) :
                                          M Unit
                                          Equations
                                            Instances For
                                              source
                                              def Lean.IR.Checker.checkJP (j : JoinPointId) :
                                              M Unit
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.IR.Checker.checkArg (a : Arg) :
                                                  M Unit
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.IR.Checker.checkArgs (as : Array Arg) :
                                                      M Unit
                                                      Equations
                                                        Instances For
                                                          source
                                                          @[inline]
                                                          def Lean.IR.Checker.checkEqTypes (ty₁ ty₂ : IRType) :
                                                          M Unit
                                                          Equations
                                                            Instances For
                                                              source
                                                              @[inline]
                                                              def Lean.IR.Checker.checkType (ty : IRType) (p : IRType → Bool) (suffix? : Option String := none) :
                                                              M Unit
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lean.IR.Checker.checkObjType (ty : IRType) :
                                                                  M Unit
                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Lean.IR.Checker.checkScalarType (ty : IRType) :
                                                                      M Unit
                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def Lean.IR.Checker.getType (x : VarId) :
                                                                          M IRType
                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              @[inline]
                                                                              def Lean.IR.Checker.checkVarType (x : VarId) (p : IRType → Bool) (suffix? : Option String := none) :
                                                                              M Unit
                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def Lean.IR.Checker.checkObjVar (x : VarId) :
                                                                                  M Unit
                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      def Lean.IR.Checker.checkScalarVar (x : VarId) :
                                                                                      M Unit
                                                                                      Equations
                                                                                        Instances For
                                                                                          source
                                                                                          def Lean.IR.Checker.checkFullApp (c : FunId) (ys : Array Arg) :
                                                                                          M Unit
                                                                                          Equations
                                                                                            Instances For
                                                                                              source
                                                                                              def Lean.IR.Checker.checkPartialApp (c : FunId) (ys : Array Arg) :
                                                                                              M Unit
                                                                                              Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  def Lean.IR.Checker.checkExpr (ty : IRType) :
                                                                                                  Expr → M Unit
                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      @[inline]
                                                                                                      def Lean.IR.Checker.withParams (ps : Array Param) (k : M Unit) :
                                                                                                      M Unit
                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          source
                                                                                                          partial def Lean.IR.Checker.checkFnBody :
                                                                                                          FnBody → M Unit
                                                                                                          source
                                                                                                          def Lean.IR.Checker.checkDecl :
                                                                                                          Decl → M Unit
                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Lean.IR.checkDecl (decls : Array Decl) (decl : Decl) :
                                                                                                              CompilerM Unit
                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def Lean.IR.checkDecls (decls : Array Decl) :
                                                                                                                  CompilerM Unit
                                                                                                                  Equations
                                                                                                                    Instances For