March equinox🍃👒

I almost forgot about mastodon and buried in work for a long time. Stop it and post a Toot. :mastodon:

@Brian_Mahoney Happy New Year🧧🏮

Happy Chinese New Year 🧧🏮
Year of the Snake 🐍 ㊗️
#YearOfTheSnake

@siegie Happy New Year🧧🏮

@gero1965 Happy New Year 🏮㊗️

New Year's Eve Dinner🍷 I celebrated Chinese New Year 🏮 with my team 🧧 in Shanghai Peace Hotel 🏨

Lonely white in winter 🤍🌹

macOS Sequoia menu bar occasional render error 🟥

GPU render error on Safari 18.2! 🟥

Goodbye Monterey, which has been with me for 4 years. Hello Sequoia

My 2025 startup at Jan 15th. I had a long Christmas break and missing for some time.

@mars1024 To be best

@ErikUden Merry Christmas 🎁

@jroberts Yep, Olive green and red roof are elegant combination

My Christmas gift is a Mini Cooper🚗
#Christmas

Join mastodon 2 years old today...
#mastodon

Damascus is your dreamland,
you also want to stay in the presidential suite.
But you just only dream about it,
you still have to go to work
after waking up on Monday.

Church has a λI system; the difference from λ is that vacuous abstraction is prohibited. When constructing λx.M, x must be a free var of M. From the perspective of type (CHC), abstraction is an implication-intro rule, and prohibiting vacuous abstraction is equivalent to requiring that A must be discharged in natural deduction, that is, it must be A -> B instead of [A] -> B, which prohibits the weakening rule.

I make this solution