Toot

Written by Lîm Tsú-thuàn on 2025-01-26 at 11:09

@zyang @anuytstt For free variables occurs at initial term, I already see it can fail, e.g.

(\x. \y. x) y = \y. y (oops)

so if we disallow free variables (all are bound now), then?

=> More informations about this toot | View the thread | More toots from dannypsnl@g0v.social

Mentions

=> View zyang@mathstodon.xyz profile | View anuytstt@fosstodon.org profile

Tags