mathlib documentation

data.buffer.parser.numeral

Numeral parsers #

This file expands on the existing nat : parser to provide parsers into any type α that can be represented by a numeral, which relies on α having a 0, 1, and addition operation. There are also convenience parsers that ensure that the numeral parsed in is not larger than the cardinality of the type α , if it is known that fintype α. Additionally, there are convenience parsers that parse in starting from "1", which can be useful for positive ordinals; or parser from a given character or character range.

Main definitions #

Implementation details #

When the numeral or related parsers are invoked, the desired type is provided explicitly. In many cases, it can be inferred, so one can write, for example

def get_fin : string  fin 5 :=
sum.elim (λ _, 0) id  parser.run_string (parser.numeral.of_fintype _)

In the definitions of the parsers (except for numeral), there is an explicit nat.bin_cast instead an explicit or implicit nat.cast

@[instance]
def parser.numeral.mono (α : Type) [has_zero α] [has_one α] [has_add α] :
@[instance]
def parser.numeral.prog (α : Type) [has_zero α] [has_one α] [has_add α] :
@[instance]
def parser.numeral.bounded (α : Type) [has_zero α] [has_one α] [has_add α] :
def parser.numeral (α : Type) [has_zero α] [has_one α] [has_add α] :

Parse a string of digits as a numeral while casting it to target type α.

Equations
def parser.numeral.of_fintype (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

Parse a string of digits as a numeral while casting it to target type α, which has a [fintype α] constraint. The parser ensures that the numeral parsed in is within the cardinality of the type α.

Equations
@[instance]
@[instance]
@[instance]
@[instance]
def parser.numeral.from_one (α : Type) [has_zero α] [has_one α] [has_add α] :

Parse a string of digits as a numeral while casting it to target type α. The parsing starts at "1", so "1" is parsed in as nat.cast 0. Providing "0" to the parser causes a failure.

Equations
def parser.numeral.from_one.of_fintype (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] :

Parse a string of digits as a numeral while casting it to target type α, which has a [fintype α] constraint. The parser ensures that the numeral parsed in is within the cardinality of the type α. The parsing starts at "1", so "1" is parsed in as nat.cast 0. Providing "0" to the parser causes a failure.

Equations
@[instance]
def parser.numeral.char.step (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :
(parser.numeral.char α fromc toc).step
@[instance]
def parser.numeral.char.err_static (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :
def parser.numeral.char (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :

Parse a character as a numeral while casting it to target type α, The parser ensures that the character parsed in is within the bounds set by fromc and toc, and subtracts the value of fromc from the parsed in character.

Equations
@[instance]
def parser.numeral.char.mono (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :
(parser.numeral.char α fromc toc).mono
@[instance]
def parser.numeral.char.bounded (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :
@[instance]
def parser.numeral.char.of_fintype.step (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] (fromc : char) :
@[instance]
def parser.numeral.char.of_fintype.mono (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] (fromc : char) :
def parser.numeral.char.of_fintype (α : Type) [has_zero α] [has_one α] [has_add α] [fintype α] (fromc : char) :

Parse a character as a numeral while casting it to target type α, which has a [fintype α] constraint. The parser ensures that the character parsed in is greater or equal to fromc and and subtracts the value of fromc from the parsed in character. There is also a check that the resulting value is within the cardinality of the type α.

Equations
@[instance]
@[instance]