Conversation

What does = mean? Equality of terms, I now get. Equality of types still scares me.

xenaproject.wordpress.com

Equality, specifications, and implementations

There are lots of kinds of equalities in Lean. Here’s some basic things that a mathematician needs to know to understand what’s going on

This Tweet was deleted by the Tweet author. Learn more

Replying to

and

Thanks for bringing up the “definitional equality is quite bad for software development” thing too - it's something I've been pondering too. Attempted to talk about it here, for instance:

Quote Tweet

Brendan Zabarauskas

@brendanzab

· Jun 19, 2020

Replying to @taktoa1 and @andrasKovacs6

Yeah, I mentioned how changing the function definition of + can break client code, even if the type signature does not change. This is a pretty weird default behaviour for most programmers!

11:29 PM · Jul 3, 2020Twitter Web App

Replying to

It's a double-edged sword – definitional equality being automatic means that you *can* refactor the definition of +, for example by using a recursion combinator rather than pattern-matching.

This Tweet was deleted by the Tweet author. Learn more

Show replies