`sumbool`

TypeObjects of the type `sumbool`

written like `{A}`

`+`

`{B}`

, is either a proof of `A`

or a proof of `B`

. They can be thought of “evidence-carrying booleans.”

If we are able prove `∀`

`(a`

`b`

`:`

`T),`

`{a`

`=`

`b}`

`+`

`{a`

`≠`

`b}`

, we say that equality is *decidable* between objects of type `T`

.

In Coq, we can use `Notation`

to modify the behavior of the parser, to provide abbreviations of terms. The notation (the string after `Notation`

) consists of tokens separated by spaces. Tokens which are identifiers (such as “A”, “x0”) are the *parameters* of the notation. Each of them must occur at least once in the abbreviated term. The other elements of the string (such as “/”) are the *symbols*. In some cases, for example in `"'IF'`

`c1`

`'then'`

`c2`

`'else'`

`c3"`

, groups of characters must be quoted to be treated as symbols.

To avoid ambiguities in expressions like `A`

`∧`

`B`

`∨`

`A`

`∨`

`C`

, we use *syntax modifiers*. We can fix this example by specifying precedence and associativity like `(at`

`level`

`..,`

`right`

`associativity)`

.

Sometimes we need to parse expressions like `x`

`!->`

`v`

`;`

`m`

and to parse subexpressions (`x`

`!->`

`v`

and `v`

`;`

`m`

) differently from when they are used separately. In this case, we must sometimes specify `at`

`next`

`level`

like in…

```
Notation "x !-> v ; m" := (t_update m x v)
(at level 100, v at next level, right associativity).
```

…but currently I have no idea of what’s happening. Coq uses Camlp5 as its parser, which is an LL(1) parser. I’ll try to explain this after figuring out how LL(1) parsers work.

We can use functions rather than lists of key-value pairs to build maps. This will give us a more extensional view of maps.

Since partial maps are just total maps (with `None`

as the default value), basic lemmas about total maps can easily be lift to fit partial maps.