1883c9b7eb
Given the derived `Repr` instance for types with parameters, the absence of `Repr Empty` can cause `Repr` instance synthesis to fail. For example, given ```lean inductive Prim (special : Type) where | plus | other : special → Prim special deriving Repr ``` this works: ```lean #eval (Prim.plus : Prim Int) ``` but this fails: ```lean #eval (Prim.plus : Prim Empty) ``` --------- Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
29 lines
665 B
Text
29 lines
665 B
Text
/-!
|
|
# Validation of `Repr Empty` instance
|
|
|
|
While it may seem unnecessary to have Repr, it prevents the automatic derivation
|
|
of Repr for other types when `Empty` is used as a type parameter.
|
|
|
|
This is a simplified version of an example from the "Functional Programming in Lean" book.
|
|
The Empty type is used to exlude the `other` constructor from the `Prim` type.
|
|
-/
|
|
|
|
inductive Prim (special : Type) where
|
|
| plus
|
|
| minus
|
|
| other : special → Prim special
|
|
deriving Repr
|
|
|
|
/-!
|
|
Check that both Repr's work
|
|
-/
|
|
|
|
/-- info: Prim.plus -/
|
|
#guard_msgs in
|
|
open Prim in
|
|
#eval (plus : Prim Int)
|
|
|
|
/-- info: Prim.minus -/
|
|
#guard_msgs in
|
|
open Prim in
|
|
#eval (minus : Prim Empty)
|