Documentation

Lean.Class

An entry for the persistent environment extension for declared type classes

Instances For
    Equations
      Instances For

        State of the type class environment extension.

        Instances For
          Equations
            Instances For

              Switch the state into persistent mode. We switch to this mode after we read all imported .olean files. Recall that we use a SMap for implementing the state of the type class environment extension.

              Equations
                Instances For
                  @[export lean_is_class]
                  def Lean.isClass (env : Environment) (n : Name) :

                  Return true if n is the name of type class in the given environment.

                  Equations
                    Instances For

                      If declName is a class, return the position of its outParams.

                      Equations
                        Instances For
                          @[export lean_has_out_params]
                          def Lean.hasOutParams (env : Environment) (declName : Name) :

                          Return true if the given declName is a type class with output parameters.

                          Equations
                            Instances For
                              @[export lean_mk_outparam_args_implicit]

                              Mark outParams in type as implicit. Note that it also marks instance implicit arguments that depend on outParams as implicit.

                              Remark: this function consumes the outParam annotations.

                              This function uses the same logic used as checkOutParam. See issue #1901

                              Equations
                                Instances For
                                  partial def Lean.mkOutParamArgsImplicit.go (type typeAux : Expr) (outParamFVarIds : Array FVarId) :

                                  Add a new type class with the given name to the environment. declName must not be the name of an existing type class, and it must be the name of constant in env. declName must be a inductive datatype or axiom. Recall that all structures are inductive datatypes.

                                  Equations
                                    Instances For