Documentation

Lean.Data.Options

Equations
    Instances For
      Equations
        Instances For
          Instances For
            Equations
              Instances For
                @[export lean_register_option]
                def Lean.registerOption (name : Name) (decl : OptionDecl) :
                Equations
                  Instances For
                    Equations
                      Instances For
                        @[export lean_get_option_decls_array]
                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        class Lean.MonadOptions (m : TypeType) :
                                        Instances
                                          def Lean.getBoolOption {m : TypeType} [Monad m] [MonadOptions m] (k : Name) (defValue : Bool := false) :
                                          Equations
                                            Instances For
                                              def Lean.getNatOption {m : TypeType} [Monad m] [MonadOptions m] (k : Name) (defValue : Nat := 0) :
                                              m Nat
                                              Equations
                                                Instances For
                                                  class Lean.MonadWithOptions (m : TypeType) :
                                                  Instances

                                                    Remark: _inPattern is an internal option for communicating to the delaborator that the term being delaborated should be treated as a pattern.

                                                    def Lean.withInPattern {m : TypeType} {α : Type} [MonadWithOptions m] (x : m α) :
                                                    m α
                                                    Equations
                                                      Instances For
                                                        Equations
                                                          Instances For
                                                            structure Lean.Option (α : Type) :

                                                            A strongly-typed reference to an option.

                                                            • name : Name
                                                            • defValue : α
                                                            Instances For
                                                              Equations
                                                                structure Lean.Option.Decl (α : Type) :
                                                                Instances For
                                                                  def Lean.Option.get? {α : Type} [KVMap.Value α] (opts : Options) (opt : Lean.Option α) :
                                                                  Equations
                                                                    Instances For
                                                                      def Lean.Option.get {α : Type} [KVMap.Value α] (opts : Options) (opt : Lean.Option α) :
                                                                      α
                                                                      Equations
                                                                        Instances For
                                                                          def Lean.Option.set {α : Type} [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) :
                                                                          Equations
                                                                            Instances For
                                                                              def Lean.Option.setIfNotSet {α : Type} [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) :

                                                                              Similar to set, but update opts only if it doesn't already contains an setting for opt.name

                                                                              Equations
                                                                                Instances For
                                                                                  def Lean.Option.register {α : Type} [KVMap.Value α] (name : Name) (decl : Option.Decl α) (ref : Name := by exact decl_name%) :
                                                                                  Equations
                                                                                    Instances For