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
              @[inline, reducible]
              abbrev Lean.IR.Checker.M (α : Type) :
              Type
              Instances For
                source
                def Lean.IR.Checker.markIndex (i : Lean.IR.Index) :
                Lean.IR.Checker.M Unit
                Instances For
                  source
                  def Lean.IR.Checker.markVar (x : Lean.IR.VarId) :
                  Lean.IR.Checker.M Unit
                  Instances For
                    source
                    def Lean.IR.Checker.markJP (j : Lean.IR.JoinPointId) :
                    Lean.IR.Checker.M Unit
                    Instances For
                      source
                      def Lean.IR.Checker.getDecl (c : Lake.Name) :
                      Lean.IR.Checker.M Lean.IR.Decl
                      Instances For
                        source
                        def Lean.IR.Checker.checkVar (x : Lean.IR.VarId) :
                        Lean.IR.Checker.M Unit
                        Instances For
                          source
                          def Lean.IR.Checker.checkJP (j : Lean.IR.JoinPointId) :
                          Lean.IR.Checker.M Unit
                          Instances For
                            source
                            def Lean.IR.Checker.checkArg (a : Lean.IR.Arg) :
                            Lean.IR.Checker.M Unit
                            Instances For
                              source
                              def Lean.IR.Checker.checkArgs (as : Array Lean.IR.Arg) :
                              Lean.IR.Checker.M Unit
                              Instances For
                                source
                                @[inline]
                                def Lean.IR.Checker.checkEqTypes (ty₁ : Lean.IR.IRType) (ty₂ : Lean.IR.IRType) :
                                Lean.IR.Checker.M Unit
                                Instances For
                                  source
                                  @[inline]
                                  def Lean.IR.Checker.checkType (ty : Lean.IR.IRType) (p : Lean.IR.IRType → Bool) (suffix? : optParam (Option String) none) :
                                  Lean.IR.Checker.M Unit
                                  Instances For
                                    source
                                    def Lean.IR.Checker.checkObjType (ty : Lean.IR.IRType) :
                                    Lean.IR.Checker.M Unit
                                    Instances For
                                      source
                                      def Lean.IR.Checker.checkScalarType (ty : Lean.IR.IRType) :
                                      Lean.IR.Checker.M Unit
                                      Instances For
                                        source
                                        def Lean.IR.Checker.getType (x : Lean.IR.VarId) :
                                        Lean.IR.Checker.M Lean.IR.IRType
                                        Instances For
                                          source
                                          @[inline]
                                          def Lean.IR.Checker.checkVarType (x : Lean.IR.VarId) (p : Lean.IR.IRType → Bool) (suffix? : optParam (Option String) none) :
                                          Lean.IR.Checker.M Unit
                                          Instances For
                                            source
                                            def Lean.IR.Checker.checkObjVar (x : Lean.IR.VarId) :
                                            Lean.IR.Checker.M Unit
                                            Instances For
                                              source
                                              def Lean.IR.Checker.checkScalarVar (x : Lean.IR.VarId) :
                                              Lean.IR.Checker.M Unit
                                              Instances For
                                                source
                                                def Lean.IR.Checker.checkFullApp (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg) :
                                                Lean.IR.Checker.M Unit
                                                Instances For
                                                  source
                                                  def Lean.IR.Checker.checkPartialApp (c : Lean.IR.FunId) (ys : Array Lean.IR.Arg) :
                                                  Lean.IR.Checker.M Unit
                                                  Instances For
                                                    source
                                                    def Lean.IR.Checker.checkExpr (ty : Lean.IR.IRType) :
                                                    Lean.IR.Expr → Lean.IR.Checker.M Unit
                                                    Instances For
                                                      source
                                                      @[inline]
                                                      def Lean.IR.Checker.withParams (ps : Array Lean.IR.Param) (k : Lean.IR.Checker.M Unit) :
                                                      Lean.IR.Checker.M Unit
                                                      Instances For
                                                        source
                                                        partial def Lean.IR.Checker.checkFnBody :
                                                        Lean.IR.FnBody → Lean.IR.Checker.M Unit
                                                        source
                                                        def Lean.IR.Checker.checkDecl :
                                                        Lean.IR.Decl → Lean.IR.Checker.M Unit
                                                        Instances For
                                                          source
                                                          def Lean.IR.checkDecl (decls : Array Lean.IR.Decl) (decl : Lean.IR.Decl) :
                                                          Lean.IR.CompilerM Unit
                                                          Instances For
                                                            source
                                                            def Lean.IR.checkDecls (decls : Array Lean.IR.Decl) :
                                                            Lean.IR.CompilerM Unit
                                                            Instances For