Documentation

Lean.Elab.ConfigEval.Instances

Evaluator instances for built-in types #

Some of these instances are hand-written instead of being derived, since the syntax may be special, or they might make special assumptions on the type (e.g. for Bool, we assume the identifiers true and false always refer to Bool's constructors).

EvalTerm instances #

source
def Lean.Elab.ConfigEval.EvalTerm.evalBoolStx :
Term → TermElabM (Bool × Expr)
Instances For
    source
    def Lean.Elab.ConfigEval.EvalTerm.evalNatStx :
    Term → TermElabM (Nat × Expr)
    Instances For
      source
      def Lean.Elab.ConfigEval.EvalTerm.evalIntStx :
      Term → TermElabM (Int × Expr)
      Instances For
        source
        def Lean.Elab.ConfigEval.EvalTerm.evalStringStx :
        Term → TermElabM (String × Expr)
        Instances For
          source
          def Lean.Elab.ConfigEval.EvalTerm.evalNameStx :
          Term → TermElabM (Name × Expr)
          Instances For
            source
            def Lean.Elab.ConfigEval.EvalTerm.evalOptionStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) :
            Term → TermElabM (Option α × Expr)
            Instances For
              source
              def Lean.Elab.ConfigEval.EvalTerm.evalListStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) :
              Term → TermElabM (List α × Expr)
              Instances For
                source
                def Lean.Elab.ConfigEval.EvalTerm.evalArrayStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) :
                Term → TermElabM (Array α × Expr)
                Instances For
                  source
                  def Lean.Elab.ConfigEval.EvalTerm.evalProdStx {α α' : Type} (typeExpr typeExpr' : Expr) (ev : Term → TermElabM (α × Expr)) (ev' : Term → TermElabM (α' × Expr)) :
                  Term → TermElabM ((α × α') × Expr)
                  Instances For
                    source
                    def Lean.Elab.ConfigEval.EvalTerm.evalDataValueStx (stx : Term) :
                    TermElabM (DataValue × Expr)
                    Instances For
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instBool :
                      EvalTerm Bool
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instNat :
                      EvalTerm Nat
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instInt :
                      EvalTerm Int
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instString :
                      EvalTerm String
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instName :
                      EvalTerm Name
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instOption {α : Type} [EvalTerm α] :
                      EvalTerm (Option α)
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instList {α : Type} [EvalTerm α] :
                      EvalTerm (List α)
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instArray {α : Type} [EvalTerm α] :
                      EvalTerm (Array α)
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instProd {α α' : Type} [EvalTerm α] [EvalTerm α'] :
                      EvalTerm (α × α')
                      source
                      @[implicit_reducible]
                      instance Lean.Elab.ConfigEval.EvalTerm.instDataValue :
                      EvalTerm DataValue

                      EvalExpr instances #

                      source
                      def Lean.Elab.ConfigEval.EvalExpr.evalBoolExprCore (e : Expr) :
                      MetaM Bool
                      Instances For
                        source
                        def Lean.Elab.ConfigEval.EvalExpr.evalBoolExpr :
                        Expr → MetaM Bool
                        Instances For
                          source
                          def Lean.Elab.ConfigEval.EvalExpr.evalNatExprCore (e : Expr) :
                          MetaM Nat
                          Instances For
                            source
                            def Lean.Elab.ConfigEval.EvalExpr.evalNatExpr :
                            Expr → MetaM Nat
                            Instances For
                              source
                              def Lean.Elab.ConfigEval.EvalExpr.evalIntExprCore (e : Expr) :
                              MetaM Int
                              Instances For
                                source
                                def Lean.Elab.ConfigEval.EvalExpr.evalIntExpr :
                                Expr → MetaM Int
                                Instances For
                                  source
                                  def Lean.Elab.ConfigEval.EvalExpr.evalStringExprCore :
                                  Expr → MetaM String
                                  Instances For
                                    source
                                    def Lean.Elab.ConfigEval.EvalExpr.evalStringExpr :
                                    Expr → MetaM String
                                    Instances For
                                      source
                                      def Lean.Elab.ConfigEval.EvalExpr.evalNameExprCore (e : Expr) :
                                      MetaM Name
                                      Instances For
                                        source
                                        def Lean.Elab.ConfigEval.EvalExpr.evalNameExpr :
                                        Expr → MetaM Name
                                        Instances For
                                          source
                                          def Lean.Elab.ConfigEval.EvalExpr.evalOptionExprCore {α : Type} (ev : Expr → MetaM α) (e : Expr) :
                                          MetaM (Option α)
                                          Instances For
                                            source
                                            def Lean.Elab.ConfigEval.EvalExpr.evalOptionExpr {α : Type} (ev : Expr → MetaM α) (e : Expr) :
                                            MetaM (Option α)
                                            Instances For
                                              source
                                              partial def Lean.Elab.ConfigEval.EvalExpr.evalListExpr {α : Type} (ev : Expr → MetaM α) (e : Expr) (didWHNF : Bool := false) :
                                              MetaM (List α)
                                              source
                                              def Lean.Elab.ConfigEval.EvalExpr.evalArrayExpr {α : Type} (ev : Expr → MetaM α) :
                                              Expr → MetaM (Array α)
                                              Instances For
                                                source
                                                def Lean.Elab.ConfigEval.EvalExpr.evalDataValueExprCore (e : Expr) :
                                                MetaM DataValue
                                                Instances For
                                                  source
                                                  def Lean.Elab.ConfigEval.EvalExpr.evalDataValueExpr :
                                                  Expr → MetaM DataValue
                                                  Instances For
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instBool :
                                                    EvalExpr Bool
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instNat :
                                                    EvalExpr Nat
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instInt :
                                                    EvalExpr Int
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instString :
                                                    EvalExpr String
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instName :
                                                    EvalExpr Name
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instOption {α : Type} [EvalExpr α] :
                                                    EvalExpr (Option α)
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instList {α : Type} [EvalExpr α] :
                                                    EvalExpr (List α)
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instArray {α : Type} [EvalExpr α] :
                                                    EvalExpr (Array α)
                                                    source
                                                    @[implicit_reducible]
                                                    instance Lean.Elab.ConfigEval.EvalExpr.instDataValue :
                                                    EvalExpr DataValue