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
Instances For
    source
    @[extern lean_get_max_ctor_scalars_size]
    opaque Lean.IR.Checker.getMaxCtorScalarsSize :
    Unit → Nat
    source
    def Lean.IR.Checker.maxCtorScalarsSize :
    Nat
    Instances For
      source
      @[extern lean_get_max_ctor_tag]
      opaque Lean.IR.Checker.getMaxCtorTag :
      Unit → Nat
      source
      def Lean.IR.Checker.maxCtorTag :
      Nat
      Instances For
        source
        @[extern lean_get_usize_size]
        opaque Lean.IR.Checker.getUSizeSize :
        Unit → Nat
        source
        def Lean.IR.Checker.usizeSize :
        Nat
        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
              Instances For
                source
                def Lean.IR.Checker.throwCheckerError {α : Type} (msg : String) :
                M α
                Instances For
                  source
                  def Lean.IR.Checker.markIndex (i : Index) :
                  M Unit
                  Instances For
                    source
                    def Lean.IR.Checker.markVar (x : VarId) :
                    M Unit
                    Instances For
                      source
                      def Lean.IR.Checker.markJP (j : JoinPointId) :
                      M Unit
                      Instances For
                        source
                        def Lean.IR.Checker.getDecl (c : Name) :
                        M Decl
                        Instances For
                          source
                          def Lean.IR.Checker.checkVar (x : VarId) :
                          M Unit
                          Instances For
                            source
                            def Lean.IR.Checker.checkJP (j : JoinPointId) :
                            M Unit
                            Instances For
                              source
                              def Lean.IR.Checker.checkArg (a : Arg) :
                              M Unit
                              Instances For
                                source
                                def Lean.IR.Checker.checkArgs (as : Array Arg) :
                                M Unit
                                Instances For
                                  source
                                  @[inline]
                                  def Lean.IR.Checker.checkEqTypes (ty₁ ty₂ : IRType) :
                                  M Unit
                                  Instances For
                                    source
                                    @[inline]
                                    def Lean.IR.Checker.checkType (ty : IRType) (p : IRType → Bool) (suffix? : Option String := none) :
                                    M Unit
                                    Instances For
                                      source
                                      def Lean.IR.Checker.checkObjType (ty : IRType) :
                                      M Unit
                                      Instances For
                                        source
                                        def Lean.IR.Checker.checkScalarType (ty : IRType) :
                                        M Unit
                                        Instances For
                                          source
                                          def Lean.IR.Checker.getType (x : VarId) :
                                          M IRType
                                          Instances For
                                            source
                                            @[inline]
                                            def Lean.IR.Checker.checkVarType (x : VarId) (p : IRType → Bool) (suffix? : Option String := none) :
                                            M Unit
                                            Instances For
                                              source
                                              def Lean.IR.Checker.checkObjVar (x : VarId) :
                                              M Unit
                                              Instances For
                                                source
                                                def Lean.IR.Checker.checkScalarVar (x : VarId) :
                                                M Unit
                                                Instances For
                                                  source
                                                  def Lean.IR.Checker.checkFullApp (c : FunId) (ys : Array Arg) :
                                                  M Unit
                                                  Instances For
                                                    source
                                                    def Lean.IR.Checker.checkPartialApp (c : FunId) (ys : Array Arg) :
                                                    M Unit
                                                    Instances For
                                                      source
                                                      def Lean.IR.Checker.checkExpr (ty : IRType) (e : Expr) :
                                                      M Unit
                                                      Instances For
                                                        source
                                                        @[inline]
                                                        def Lean.IR.Checker.withParams (ps : Array Param) (k : M Unit) :
                                                        M Unit
                                                        Instances For
                                                          source
                                                          partial def Lean.IR.Checker.checkFnBody (fnBody : FnBody) :
                                                          M Unit
                                                          source
                                                          def Lean.IR.Checker.checkDecl :
                                                          Decl → M Unit
                                                          Instances For
                                                            source
                                                            def Lean.IR.checkDecl (decls : Array Decl) (decl : Decl) :
                                                            CompilerM Unit
                                                            Instances For
                                                              source
                                                              def Lean.IR.checkDecls (decls : Array Decl) :
                                                              CompilerM Unit
                                                              Instances For