Difference between revisions of "Notation"

Revision as of 09:06, 3 November 2022

v : τ means value v has type τ.
X = a means that a type or a value X is an alias for a.
X := [something] means that X is defined to be [something]
A percent sign % preceded only by spaces starts a line comment % [comment]
We use · to denote that we do not care about the value some variable takes. For example, when quantifying over a set of tuples of the form [math]\displaystyle{ (x, y) }[/math] we may use a [math]\displaystyle{ (x, \cdot) }[/math] to express that we do not care about the value [math]\displaystyle{ y }[/math] takes in each of the tuples.
Let [math]\displaystyle{ X }[/math] be a set or a sequence. We use [math]\displaystyle{ |X| }[/math] to denote the size/length of the set/sequence.

@@ Line 2: / Line 2: @@
 * <code>v : τ</code> means value <code>v</code> has type <code>τ</code>.
+* <code>X = a</code> means that a type or a value <code>X</code> is an alias for <code>a</code>.
+* <code>X := [something]</code> means that <code>X</code> is defined to be <code>[something]</code>
+* A percent sign <code>%</code> preceded only by spaces starts a line comment <code>% [comment]</code>
+* We use <code>·</code> to denote that we do not care about the value some variable takes. For example, when quantifying over a set of tuples of the form <math>(x, y)</math> we may use a <math>(x, \cdot)</math> to express that we do not care about the value <math>y</math> takes in each of the tuples.
+* Let <math>X</math> be a set or a sequence. We use <math>|X|</math> to denote the size/length of the set/sequence.