there was a time where roughly this time on Friday there was a thread about some funny behaviour in Lean. I do not know if this has been brought up before, but the following "every type is finite in Lean" made me laugh!
import Mathlib.Data.Finite.Basic
example {α} : Finite α := inferInstance
Do not spoil the fun for others, when you realize what is going on, please! Use spoiler-blocks for compromising comments!
Seasawher
commented
3 months ago
—-
Dear All,
there was a time where roughly this time on Friday there was a thread about some funny behaviour in Lean. I do not know if this has been brought up before, but the following "every type is finite in Lean" made me laugh!
Do not spoil the fun for others, when you realize what is going on, please! Use
spoiler-blocks for compromising comments!