Equations
Instances For
consume a newline character sequence pretending, that we read '\n'. As per spec: https://www.w3.org/TR/xml/#sec-line-ends
Equations
- Lean.Xml.Parser.endl = (Std.Internal.Parsec.String.skipString "\x0d\n" <|> Std.Internal.Parsec.String.skipChar '\x0d' <|> Std.Internal.Parsec.String.skipChar '\n') *> pure '\n'
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-Char
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-NameStartChar
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-NameChar
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-EncName
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-SDDecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-XMLDecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-Comment
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-PITarget
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-PI
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-Misc
Equations
- Lean.Xml.Parser.Misc = (Lean.Xml.Parser.Comment *> pure () <|> Lean.Xml.Parser.PI <|> Lean.Xml.Parser.S *> pure ())
Instances For
https://www.w3.org/TR/xml/#NT-SystemLiteral
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-PubidChar
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-PubidLiteral
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-ExternalID
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-Mixed
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-children
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-elementdecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-TokenizedType
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-NotationType
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-Enumeration
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Xml.Parser.predefinedEntityToChar "lt" = some '<'
- Lean.Xml.Parser.predefinedEntityToChar "gt" = some '>'
- Lean.Xml.Parser.predefinedEntityToChar "amp" = some '&'
- Lean.Xml.Parser.predefinedEntityToChar "apos" = some '''
- Lean.Xml.Parser.predefinedEntityToChar "quot" = some '\"'
- Lean.Xml.Parser.predefinedEntityToChar x = none
Instances For
Equations
- Lean.Xml.Parser.hexDigitToNat c = if '0' ≤ c ∧ c ≤ '9' then Char.toNat c - '0'.toNat else if 'a' ≤ c ∧ c ≤ 'f' then Char.toNat c - 'a'.toNat + 10 else Char.toNat c - 'A'.toNat + 10
Instances For
Equations
- Lean.Xml.Parser.digitsToNat base digits = Array.foldl (fun (r d : Nat) => r * base + d) 0 digits
Instances For
https://www.w3.org/TR/xml/#NT-CharRef
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-AttValue
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-DefaultDecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-AttlistDecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-EntityValue
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-GEDecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-PEDecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-NotationDecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-markupdecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-doctypedecl
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-prolog
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-Attribute
Equations
- Lean.Xml.Parser.Attribute = do let name ← Lean.Xml.Parser.Name Lean.Xml.Parser.Eq let value ← Lean.Xml.Parser.AttValue pure (name, value)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-EmptyElemTag
Equations
- Lean.Xml.Parser.EmptyElemTag elem = Std.Internal.Parsec.String.skipString "/>" *> pure (elem #[])
Instances For
https://www.w3.org/TR/xml/#NT-STag
Equations
- Lean.Xml.Parser.STag elem = Std.Internal.Parsec.String.skipChar '>' *> pure elem
Instances For
https://www.w3.org/TR/xml/#NT-CData
Equations
- Lean.Xml.Parser.CData = (Std.Internal.Parsec.notFollowedBy (Std.Internal.Parsec.String.skipString "]]>") *> Std.Internal.Parsec.any).manyChars
Instances For
https://www.w3.org/TR/xml/#NT-CharData
Equations
- One or more equations did not get rendered due to their size.
Instances For
https://www.w3.org/TR/xml/#NT-document
Equations
- Lean.Xml.Parser.document = Lean.Xml.Parser.prolog *> Lean.Xml.Parser.element <* Std.Internal.Parsec.many Lean.Xml.Parser.Misc <* Std.Internal.Parsec.eof
Instances For
Equations
- Lean.Xml.parse s = Lean.Xml.Parser.document.run s