definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ].
definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].
definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ].
definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].