Title: Theory / Unimportant / CS / Programming / Coq / standard library theorem

Instruction: app_nil_end
Page: 29
Language: coq
Chapter: 2
Section: 1.4
Returns: l = l ++ nil

Instruction: app_assoc_reverse
Page: 29
Language: coq
Chapter: 2
Section: 1.4
Returns: (l ++ m) ++ n = l ++ m ++ n

Typ: unit
Meaning: Set with a single value `tt`
Page: 41
Chapter: 3
Section: 1
Context: coq

Instruction: negb
Page: 45
Language: coq
Chapter: 3
Section: 1
Returns: negation on boolean

Instruction: O
Page: 45
Language: coq
Chapter: 3
Returns: The representation of 0 as a nat

Instruction: S n
Page: 45
Language: coq
Chapter: 3
Returns: The representation of n+1 as a nat

Typ: nat
Page: 45
Language: coq
Chapter: 3
Value: O represents 0
Value2: S n: the successor of n

Instruction: isZero
Page: 45
Language: coq
Chapter: 3
Returns: property of the nat true only for O

Instruction: pred n
Page: 45
Language: coq
Chapter: 3
Returns: max (n-1, 0)
Variables: n: nat

Instruction: plus
Page: 45
Language: coq
Chapter: 3
Returns: sum on nat

Instruction: O_plus_n
Page: 45
Language: coq
Chapter: 3
Returns: plus O n = n

Instruction: n_plus_O
Page: 45
Language: coq
Chapter: 3
Returns: plus n O = n