何を言っているのか全然わからないexample (解決)

[shnarazk]

７章に出てくるexampleがわからない：

example {α : Type} [Semigroup2 α] (a b : α) : α := a ⋄ b -- (1)

知っていること：

example 仮定 : 成立すること := 証明

なのだから、αが半群でa, bがαならαは存在する???

どうもそういう事らしい：

example (a : ℕ) : ℕ := by exact a   -- aが自然数なら自然数は存在する

だそうだ。しかし、最初の式(1)から派生した下式も成立する。

example {α : Type} [Semigroup₁ α] (a _b : α) : α := by exact a

むしろ

example 仮定 : 式 := 式の実例

と考える方がいいかも知れない。Curry-Howard同型対応から

example 仮定 : 型 := 値

なのだから。

補足

byによる無名命題形式

by 証明 : 型

で書き直すと

by a ⋄ b : α

となってこれもまあそんなものだろうという気がする。