the swift programming language is my fault to some degree. mostly here to see dogs, shitpost, fix old computers, and/or talk about math and weird computer programming things. for effortposts check the #longpost pinned tag. asks are open.
yes, we are putting floats in the type system, and Foo<NaN> is a different type from Foo<NaN>
unsafeCoerce : a -> b unsafeCoerce x = rewrite owo in x where 0 T : Double -> Type T x = if x < 0 then b else a Infty = 1.0 / 0.0 uwu : -Infty === Infty uwu = let zz : -0.0 === 0.0 := Refl in cong (1 /) zz owo : b === a owo = cong T uwu
I worked a bit with Python type annotations and I think I got type checker to say
incompatible type "Foo[X]"; expected "Foo[X]"
at least twice
