Semantics Update Syntax?

Stream: new members

[Andrew Elsey]

Hi all,

I saw this syntax in a textbook:
image.png
I'm trying to figure out how to use it. Is this real syntax or just CS notation that's misleadingly placed? Do I need to implement a type class? Trying to update a N -> Some Type environment

[Mario Carneiro]

context is important

[Mario Carneiro]

but if I had to guess, it is probably a substitution operator

[Mario Carneiro]

what was the surrounding paragraph? The textbook's topic? Symbols are very overloaded in math

[Jasmin Blanchette]

Looks like the Hitchhiker's guide to me.

[Andrew Elsey]

This fella:
image.png
It's all over the chapter. I know this is common CS notation so I wasn't sure if the book is just confusing me into believing it's syntax

[Jasmin Blanchette]

It's real Lean syntax. We've defined it in LoVelib. That's what the text says (or tries to say).

[Jasmin Blanchette]

Which happens to also coincide more or less with traditional computer science syntax.

[Jasmin Blanchette]

Does this answer your question?

[Reid Barton]

So it's the just barely visible state (probably s) modified to map the variable x to the value a s which is as described at the start of that paragraph.

[Andrew Elsey]

Oh, I see now, I have to install a library to get it, cool, will check that out. Thank you folks very much

[Jasmin Blanchette]

Ah, that clarifies it.

[Jasmin Blanchette]

LoVelib is used throughout. See the preface. ;)

[Andrew Elsey]

Yep, just grepped and saw. Will check it out. Thanks!

[Andrew Elsey]

Great book BTW