Lean can automatically generate instances for many classes, a process known as deriving instances. Instance deriving can be invoked either when defining a type or as a stand-alone command.
As part of a command that creates a new inductive type, a Lean.Parser.Command.declaration : commandderiving clause specifies a comma-separated list of class names for which instances should be generated:
optDeriving ::= (deriving derivingClass,*)?
The stand-alone Lean.Parser.Command.deriving : commandderiving command specifies a number of class names and subject names.
Each of the specified classes are derived for each of the specified subjects.
command ::= ... | deriving instance derivingClass,* for term,*
After specifying multiple classes to derive for multiple types, as in this code:
structure A where
structure B where
deriving instance BEq, Repr for A, B
all the instances exist for all the types, so all four Lean.Parser.Command.synth : command#synth commands succeed:
#synth BEq A
#synth BEq B
#synth Repr A
#synth Repr B
Instance deriving uses a table of deriving handlers that maps type class names to metaprograms that derive instances for them.
Deriving handlers may be added to the table using registerDerivingHandler, which should be called in an Lean.Parser.Command.initialize : commandinitialize block.
Each deriving handler should have the type Array Name → CommandElabM Bool.
When a user requests that an instance of a class be derived, its registered handlers are called one at a time.
They are provided with all of the names in the mutual block for which the instance is to be derived, and should either correctly derive an instance and return true or have no effect and return false.
When a handler returns true, no further handlers are called.
Lean includes deriving handlers for the following classes:
Registers a deriving handler for a class. This function should be called in an initialize block.
A DerivingHandler is called on the fully qualified names of all types it is running for. For
example, deriving instance Foo for Bar, Baz invokes fooHandler #[`Bar, `Baz].
Instances of the IsEnum class demonstrate that a type is a finite enumeration by providing a bijection between the type and a suitably-sized Fin:
class IsEnum (α : Type) where
size : Nat
toIdx : α → Fin size
fromIdx : Fin size → α
to_from_id : ∀ (i : Fin size), toIdx (fromIdx i) = i
from_to_id : ∀ (x : α), fromIdx (toIdx x) = x
For inductive types that are trivial enumerations, where no constructor expects any parameters, instances of this class are quite repetitive.
The instance for Bool is typical:
instance : IsEnum Bool where
size := 2
toIdx
| false => 0
| true => 1
fromIdx
| 0 => false
| 1 => true
to_from_id
| 0 => rfl
| 1 => rfl
from_to_id
| false => rfl
| true => rfl
The deriving handler programmatically constructs each pattern case, by analogy to the IsEnum Bool implementation:
open Lean Elab Parser Term Command
def deriveIsEnum (declNames : Array Name) : CommandElabM Bool := do
if h : declNames.size = 1 then
let env ← getEnv
if let some (.inductInfo ind) := env.find? declNames[0] then
let mut tos : Array (TSyntax ``matchAlt) := #[]
let mut froms := #[]
let mut to_froms := #[]
let mut from_tos := #[]
let mut i := 0
for ctorName in ind.ctors do
let c := mkIdent ctorName
let n := Syntax.mkNumLit (toString i)
tos := tos.push (← `(matchAltExpr| | $c => $n))
from_tos := from_tos.push (← `(matchAltExpr| | $c => rfl))
froms := froms.push (← `(matchAltExpr| | $n => $c))
to_froms := to_froms.push (← `(matchAltExpr| | $n => rfl))
i := i + 1
let cmd ← `(instance : IsEnum $(mkIdent declNames[0]) where
size := $(quote ind.ctors.length)
toIdx $tos:matchAlt*
fromIdx $froms:matchAlt*
to_from_id $to_froms:matchAlt*
from_to_id $from_tos:matchAlt*)
elabCommand cmd
return true
return false
initialize
registerDerivingHandler ``IsEnum deriveIsEnum