6.2. Instance Declarations🔗

Given this definition of NatTree:

the following BEq instance fails:

with errors in both the left and right recursive calls that read:

failed to synthesize
  BEq NatTree
Additional diagnostic information may be available using the `set_option diagnostics true` command.

Given a suitable recursive function, such as NatTree.beq:

the instance can be created in a second step:

or, equivalently, using anonymous constructor syntax:

In this definition of NatRoseTree, the type being defined occurs nested under another inductive type constructor (Array):

Checking the equality of rose trees requires checking equality of arrays. However, instances are not typically available for instance synthesis during their own definitions, so the following definition fails, even though NatRoseTree.beq is a recursive function and is in scope in its own definition.

failed to synthesize
  BEq (Array NatRoseTree)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

To solve this, a local BEq NatRoseTree instance may be let-bound:

The use of array equality on the children finds the let-bound instance during instance synthesis.

Because DecidableEq α is an abbreviation for (a b : α) → Decidable (Eq a b), its arguments can be used directly, as in this example:

The type StringList represents monomorphic lists of strings:

In the following attempt at defining a DecidableEq instance, instance synthesis invoked while elaborating the inner termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false. if fails because the instance is not available for instance synthesis in its own definition:

failed to synthesize
  Decidable (t1 = t2)
Additional diagnostic information may be available using the `set_option diagnostics true` command.

However, because it is an ordinary Lean function, it can recursively refer to its own explicitly-provided name:

A default instance of OfNat Nat is used to select Nat for natural number literals in the absence of other type information. It is declared in the Lean standard library with priority 100. Given this representation of even numbers, in which an even number is represented by half of it:

the following instances allow numeric literals to be used for small Even values (a limit on the depth of type class instance search prevents them from being used for arbitrarily large literals):

{ half := 0 }

{ half := 17 }

{ half := 127 }

Specifying them as default instances with a priority greater than or equal to 100 causes them to be used instead of Nat:

{ half := 0 }

{ half := 17 }

Non-even numerals still use the OfNat Nat instance:

5