Skip to content

Commit

Permalink
#eval の仕様変更に伴うコード例の更新
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Nov 8, 2024
1 parent 2728e4e commit 2b42bf8
Showing 1 changed file with 5 additions and 8 deletions.
13 changes: 5 additions & 8 deletions LeanByExample/Reference/Declarative/Deriving.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,16 +11,13 @@ inductive Color : Type where
| green
| blue

-- 最初は `Repr` が定義されていないので `eval` できない
-- 暗黙的に Repr インスタンスを生成しない
set_option eval.derive.repr false

-- `Repr` が定義されていないので `eval` できない
/--
error: expression
Color.red
has type
error: could not synthesize a 'Repr' or 'ToString' instance for type
Color
but instance
Lean.Eval Color
failed to be synthesized, this instance instructs Lean on how to display the resulting value,
recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
-/
#guard_msgs in #eval Color.red

Expand Down

0 comments on commit 2b42bf8

Please sign in to comment.