search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
48 stars 7 forks source link

Fin と Nat の積 #245

Closed Seasawher closed 5 months ago

Seasawher commented 5 months ago

see: https://lecopivo.github.io/scientific-computing-lean/working-with-arrays/tensor-operations.html#pooling-and-difficulties-with-dependent-types

Beware! Fin n is endowed with modular arithmetic. Naively calling 2*i would multiply i by two and perform modulo by n/2. We do not want that; we have to get the underlying natural number i.1 and multiply then by two.

実際には：

#guard (2 : Nat) * (⟨3, by omega⟩ : Fin 4) = (6 : Nat)
Seasawher commented 5 months ago

本家に issue として投稿したのでくろーず