@rahulc29 @antidote @isAdisplayName Well, in practice you implement some algorithm that is equivalent to the one you describe, but is more efficient. The problem with Lean is, to my recollection, that the definitional equality relation is very strong and includes things where you would have to invent out of thin air a proof of some proposition. When this theory is turned into an algorithm, there could be many potential impacts; for lean, I seem to recall that the impact is that there are equations that can be proved by sequencing two “refls” but not by using a single “refl”. Syntactically minded people identify this as a failure of subject reduction, but I think that description can obscure the practical impact.
=> More informations about this toot | View the thread | More toots from jonmsterling@mathstodon.xyz
=> View rahulc29@mathstodon.xyz profile | View antidote@mathstodon.xyz profile | View isAdisplayName@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).