Documentation

Lean.Data.Options

Equations
Instances For
    Equations
    Instances For
      Equations
      Instances For
        Equations
        @[export lean_register_option]
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[export lean_get_option_decls_array]
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              Instances For
                Equations
                Instances For
                  class Lean.MonadOptions (m : TypeType) :
                  Instances
                    Equations
                    • Lean.instMonadOptionsOfMonadLift = { getOptions := liftM Lean.getOptions }
                    def Lean.getBoolOption {m : TypeType} [Monad m] [Lean.MonadOptions m] (k : Lake.Name) (defValue : optParam Bool false) :
                    Equations
                    Instances For
                      def Lean.getNatOption {m : TypeType} [Monad m] [Lean.MonadOptions m] (k : Lake.Name) (defValue : optParam Nat 0) :
                      m Nat
                      Equations
                      Instances For
                        class Lean.MonadWithOptions (m : TypeType) :
                        Instances
                          Equations

                          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} [Lean.MonadWithOptions m] (x : m α) :
                          m α
                          Equations
                          Instances For
                            Equations
                            Instances For
                              structure Lean.Option (α : Type) :

                              A strongly-typed reference to an option.

                              Instances For
                                instance Lean.instInhabitedOption :
                                {a : Type} → [inst : Inhabited a] → Inhabited (Lean.Option a)
                                Equations
                                • Lean.instInhabitedOption = { default := { name := default, defValue := default } }
                                structure Lean.Option.Decl (α : Type) :
                                Instances For
                                  def Lean.Option.get? {α : Type} [Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) :
                                  Equations
                                  Instances For
                                    def Lean.Option.get {α : Type} [Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) :
                                    α
                                    Equations
                                    Instances For
                                      def Lean.Option.set {α : Type} [Lean.KVMap.Value α] (opts : Lean.Options) (opt : Lean.Option α) (val : α) :
                                      Equations
                                      Instances For
                                        def Lean.Option.setIfNotSet {α : Type} [Lean.KVMap.Value α] (opts : Lean.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
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For