mathlib3 documentation

data.buffer.parser.numeral

Numeral parsers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 parser.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 parser.numeral), there is an explicit nat.bin_cast instead an explicit or implicit nat.cast.

@[protected, instance]
def parser.numeral.mono (α : Type) [has_zero α] [has_one α] [has_add α] :
@[protected, instance]
def parser.numeral.prog (α : Type) [has_zero α] [has_one α] [has_add α] :
@[protected, instance]
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
Instances for parser.numeral
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
Instances for parser.numeral.of_fintype
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, 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
Instances for parser.numeral.from_one

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
Instances for parser.numeral.from_one.of_fintype
@[protected, instance]
def parser.numeral.char.step (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :
(parser.numeral.char α fromc toc).step
@[protected, 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
Instances for parser.numeral.char
@[protected, instance]
def parser.numeral.char.mono (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :
(parser.numeral.char α fromc toc).mono
@[protected, instance]
def parser.numeral.char.bounded (α : Type) [has_zero α] [has_one α] [has_add α] (fromc toc : char) :
@[protected, instance]
@[protected, instance]
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
Instances for parser.numeral.char.of_fintype
@[protected, instance]
@[protected, instance]

Specific numeral types #

Matches an integer, like 43 or -2. Large numbers may cause performance issues, so don't run this parser on untrusted input.

Equations

Matches an rational number, like 43/1 or -2/3. Requires that the negation is in the numerator, and that both a numerator and denominator are provided (e.g. will not match 43). Large numbers may cause performance issues, so don't run this parser on untrusted input.

Equations