YAML 1.2.2 Production Coverage

Automated cross-reference of YAML 1.2.2 productions with @[yaml_spec] annotations in lean4-yaml-verified

Total Productions

211

Annotated Rules

211

of 211 in-scope

@[yaml_spec] Entries

568

across 17 modules

Grammar Only

Out of Scope

Coverage by Chapter

Ch 5: Characters

62/62 annotated (100.0%)

Ch 6: Basic Structures

41/41 annotated (100.0%)

Ch 7: Flow Styles

58/58 annotated (100.0%)

Ch 8: Block Styles

40/40 annotated (100.0%)

Ch 9: Documents

10/10 annotated (100.0%)

# ↕	Production ↕	Section ↕	Status ↕	Parser ↕	Proofs ↕	Scanner ↕	Spec ↕	Surface ↕	Token ↕
1	c-printable	§5.1	Grammar Only				L4YAML.CharPredicates.isPrintableBool in `L4YAML/Spec/CharPredicates.lean:215` L4YAML.CharPredicates.isPrintableProp in `L4YAML/Spec/CharPredicates.lean:202`
2	nb-json	§5.1	Grammar Only			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318` L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`	L4YAML.CharPredicates.isNbJsonProp in `L4YAML/Spec/CharPredicates.lean:232` L4YAML.CharPredicates.isNbJsonBool in `L4YAML/Spec/CharPredicates.lean:240`	L4YAML.Surface.SNbDoubleChar.plain in `L4YAML/Surface/Scalars.lean:39`
3	c-byte-order-mark	§5.2	Covered			L4YAML.Scanner.scan in `L4YAML/Scanner/Scanner.lean:524`
4	c-sequence-entry	§5.3	Covered				L4YAML.CharPredicates.canStartPlainScalarBool in `L4YAML/Spec/CharPredicates.lean:365` L4YAML.CharPredicates.canStartPlainScalarProp in `L4YAML/Spec/CharPredicates.lean:379` L4YAML.CharPredicates.validPlainFirstProp in `L4YAML/Spec/CharPredicates.lean:521` L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.validPlainFirstBool in `L4YAML/Spec/CharPredicates.lean:503` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`		L4YAML.YamlToken.blockEntry in `L4YAML/Token/Token.lean:145`
5	c-mapping-key	§5.3	Covered				L4YAML.CharPredicates.canStartPlainScalarBool in `L4YAML/Spec/CharPredicates.lean:365` L4YAML.CharPredicates.canStartPlainScalarProp in `L4YAML/Spec/CharPredicates.lean:379` L4YAML.CharPredicates.validPlainFirstProp in `L4YAML/Spec/CharPredicates.lean:521` L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.validPlainFirstBool in `L4YAML/Spec/CharPredicates.lean:503` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`		L4YAML.YamlToken.key in `L4YAML/Token/Token.lean:148`
6	c-mapping-value	§5.3	Covered			L4YAML.Scanner.scanValue in `L4YAML/Scanner/SimpleKey.lean:224` L4YAML.Scanner.scanNextToken_dispatchBlockIndicators in `L4YAML/Scanner/Scanner.lean:346`	L4YAML.CharPredicates.canStartPlainScalarBool in `L4YAML/Spec/CharPredicates.lean:365` L4YAML.CharPredicates.canStartPlainScalarProp in `L4YAML/Spec/CharPredicates.lean:379` L4YAML.CharPredicates.validPlainFirstProp in `L4YAML/Spec/CharPredicates.lean:521` L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.validPlainFirstBool in `L4YAML/Spec/CharPredicates.lean:503` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`		L4YAML.YamlToken.value in `L4YAML/Token/Token.lean:151`
7	c-collect-entry	§5.3	Covered			L4YAML.Scanner.scanFlowEntry in `L4YAML/Scanner/Scanner.lean:250` L4YAML.Scanner.scanNextToken_dispatchFlowIndicators in `L4YAML/Scanner/Scanner.lean:319`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isFlowIndicatorProp in `L4YAML/Spec/CharPredicates.lean:126` L4YAML.CharPredicates.isFlowIndicatorBool in `L4YAML/Spec/CharPredicates.lean:117` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`		L4YAML.YamlToken.flowEntry in `L4YAML/Token/Token.lean:169`
8	c-sequence-start	§5.3	Covered			L4YAML.Scanner.scanFlowSequenceStart in `L4YAML/Scanner/Scanner.lean:134`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isFlowIndicatorProp in `L4YAML/Spec/CharPredicates.lean:126` L4YAML.CharPredicates.isFlowIndicatorBool in `L4YAML/Spec/CharPredicates.lean:117` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`		L4YAML.YamlToken.flowSequenceStart in `L4YAML/Token/Token.lean:157`
9	c-sequence-end	§5.3	Covered			L4YAML.Scanner.scanFlowSequenceEnd in `L4YAML/Scanner/Scanner.lean:160`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isFlowIndicatorProp in `L4YAML/Spec/CharPredicates.lean:126` L4YAML.CharPredicates.isFlowIndicatorBool in `L4YAML/Spec/CharPredicates.lean:117` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`		L4YAML.YamlToken.flowSequenceEnd in `L4YAML/Token/Token.lean:160`
10	c-mapping-start	§5.3	Covered			L4YAML.Scanner.scanFlowMappingStart in `L4YAML/Scanner/Scanner.lean:185`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isFlowIndicatorProp in `L4YAML/Spec/CharPredicates.lean:126` L4YAML.CharPredicates.isFlowIndicatorBool in `L4YAML/Spec/CharPredicates.lean:117` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`		L4YAML.YamlToken.flowMappingStart in `L4YAML/Token/Token.lean:163`
11	c-mapping-end	§5.3	Covered			L4YAML.Scanner.scanFlowMappingEnd in `L4YAML/Scanner/Scanner.lean:211`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isFlowIndicatorProp in `L4YAML/Spec/CharPredicates.lean:126` L4YAML.CharPredicates.isFlowIndicatorBool in `L4YAML/Spec/CharPredicates.lean:117` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`		L4YAML.YamlToken.flowMappingEnd in `L4YAML/Token/Token.lean:166`
12	c-comment	§5.3	Covered				L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
13	c-anchor	§5.3	Covered			L4YAML.Scanner.collectAnchorNameLoop in `L4YAML/Scanner/NodeProperties.lean:55`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
14	c-alias	§5.3	Covered			L4YAML.Scanner.collectAnchorNameLoop in `L4YAML/Scanner/NodeProperties.lean:55`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
15	c-tag	§5.3	Covered				L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
16	c-literal	§5.3	Covered				L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
17	c-folded	§5.3	Covered				L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
18	c-single-quote	§5.3	Covered			L4YAML.Scanner.scanSingleQuoted in `L4YAML/Scanner/Scalar.lean:374`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
19	c-double-quote	§5.3	Covered			L4YAML.Scanner.scanDoubleQuoted in `L4YAML/Scanner/Scalar.lean:297`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
20	c-directive	§5.3	Covered			L4YAML.Scanner.scanDirective in `L4YAML/Scanner/Document.lean:243`	L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
21	c-reserved	§5.3	Covered				L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
22	c-indicator	§5.3	Covered				L4YAML.CharPredicates.isIndicatorProp in `L4YAML/Spec/CharPredicates.lean:184` L4YAML.CharPredicates.isIndicatorBool in `L4YAML/Spec/CharPredicates.lean:160`
23	c-flow-indicator	§5.3	Covered				L4YAML.CharPredicates.isFlowIndicatorProp in `L4YAML/Spec/CharPredicates.lean:126` L4YAML.CharPredicates.isFlowIndicatorBool in `L4YAML/Spec/CharPredicates.lean:117`
24	b-line-feed	§5.4	Covered				L4YAML.CharPredicates.isLineBreakProp in `L4YAML/Spec/CharPredicates.lean:60` L4YAML.CharPredicates.isLineBreakBool in `L4YAML/Spec/CharPredicates.lean:54`
25	b-carriage-return	§5.4	Covered				L4YAML.CharPredicates.isLineBreakProp in `L4YAML/Spec/CharPredicates.lean:60` L4YAML.CharPredicates.isLineBreakBool in `L4YAML/Spec/CharPredicates.lean:54`
26	b-char	§5.4	Covered				L4YAML.CharPredicates.isLineBreakProp in `L4YAML/Spec/CharPredicates.lean:60` L4YAML.CharPredicates.isLineBreakBool in `L4YAML/Spec/CharPredicates.lean:54`
27	nb-char	§5.4	Covered			L4YAML.Scanner.skipToEndOfLine in `L4YAML/Scanner/Whitespace.lean:120` L4YAML.Scanner.scanBlockScalarSkipComment in `L4YAML/Scanner/Scalar.lean:820` L4YAML.Scanner.collectCommentTextLoop in `L4YAML/Scanner/Whitespace.lean:205` L4YAML.Scanner.collectCommentTextLoop._unary in `L4YAML/Scanner/Whitespace.lean` L4YAML.Scanner.collectLineContentLoop in `L4YAML/Scanner/Scalar.lean:734` L4YAML.Scanner.skipToContentComment in `L4YAML/Scanner/Whitespace.lean:226`
28	b-break	§5.4	Covered			L4YAML.Scanner.consumeNewline in `L4YAML/Scanner/Whitespace.lean:129`
29	b-as-line-feed	§5.4	Covered			L4YAML.Scanner.consumeNewline in `L4YAML/Scanner/Whitespace.lean:129`
30	b-non-content	§5.4	Covered			L4YAML.Scanner.scanBlockScalarConsumeNewline in `L4YAML/Scanner/Scalar.lean:845`
31	s-space	§5.5	Covered				L4YAML.CharPredicates.isIndentCharBool in `L4YAML/Spec/CharPredicates.lean:252` L4YAML.CharPredicates.isIndentCharProp in `L4YAML/Spec/CharPredicates.lean:256` L4YAML.CharPredicates.isWhiteSpaceProp in `L4YAML/Spec/CharPredicates.lean:83` L4YAML.CharPredicates.isWhiteSpaceBool in `L4YAML/Spec/CharPredicates.lean:77`
32	s-tab	§5.5	Covered				L4YAML.CharPredicates.isWhiteSpaceProp in `L4YAML/Spec/CharPredicates.lean:83` L4YAML.CharPredicates.isWhiteSpaceBool in `L4YAML/Spec/CharPredicates.lean:77`
33	s-white	§5.5	Covered				L4YAML.CharPredicates.isWhiteSpaceProp in `L4YAML/Spec/CharPredicates.lean:83` L4YAML.CharPredicates.isWhiteSpaceBool in `L4YAML/Spec/CharPredicates.lean:77`
34	ns-char	§5.5	Covered			L4YAML.Scanner.collectDirectiveNameLoop in `L4YAML/Scanner/Document.lean:87`	L4YAML.CharPredicates.canStartPlainScalarBool in `L4YAML/Spec/CharPredicates.lean:365` L4YAML.CharPredicates.canStartPlainScalarProp in `L4YAML/Spec/CharPredicates.lean:379` L4YAML.CharPredicates.validPlainFirstProp in `L4YAML/Spec/CharPredicates.lean:521` L4YAML.CharPredicates.validPlainFirstBool in `L4YAML/Spec/CharPredicates.lean:503`
35	ns-dec-digit	§5.6	Covered			L4YAML.Scanner.collectVersionMajorLoop in `L4YAML/Scanner/Document.lean:102` L4YAML.Scanner.collectVersionMinorLoop in `L4YAML/Scanner/Document.lean:117`	L4YAML.CharPredicates.isWordCharProp in `L4YAML/Spec/CharPredicates.lean:291` L4YAML.CharPredicates.isWordCharBool in `L4YAML/Spec/CharPredicates.lean:303`
36	ns-hex-digit	§5.6	Covered			L4YAML.Scanner.collectHexDigitsLoop in `L4YAML/Scanner/Scalar.lean:46`	L4YAML.CharPredicates.isUriCharProp in `L4YAML/Spec/CharPredicates.lean:316` L4YAML.CharPredicates.isUriCharBool in `L4YAML/Spec/CharPredicates.lean:328`
37	ns-ascii-letter	§5.6	Covered				L4YAML.CharPredicates.isAsciiLetterBool in `L4YAML/Spec/CharPredicates.lean:282` L4YAML.CharPredicates.isAsciiLetterProp in `L4YAML/Spec/CharPredicates.lean:274` L4YAML.CharPredicates.isWordCharProp in `L4YAML/Spec/CharPredicates.lean:291` L4YAML.CharPredicates.isWordCharBool in `L4YAML/Spec/CharPredicates.lean:303`
38	ns-word-char	§5.6	Covered			L4YAML.Scanner.collectTagHandleLoop in `L4YAML/Scanner/NodeProperties.lean:118` L4YAML.Scanner.collectTagHandleDirectiveLoop in `L4YAML/Scanner/Document.lean:132`	L4YAML.CharPredicates.isWordCharProp in `L4YAML/Spec/CharPredicates.lean:291` L4YAML.CharPredicates.isWordCharBool in `L4YAML/Spec/CharPredicates.lean:303` L4YAML.CharPredicates.isUriCharProp in `L4YAML/Spec/CharPredicates.lean:316` L4YAML.CharPredicates.isUriCharBool in `L4YAML/Spec/CharPredicates.lean:328`
39	ns-uri-char	§5.6	Covered			L4YAML.Scanner.collectTagSuffixLoop in `L4YAML/Scanner/NodeProperties.lean:102` L4YAML.Scanner.collectVerbatimTagLoop in `L4YAML/Scanner/NodeProperties.lean:86`	L4YAML.CharPredicates.isTagCharBool in `L4YAML/Spec/CharPredicates.lean:345` L4YAML.CharPredicates.isTagCharProp in `L4YAML/Spec/CharPredicates.lean:336` L4YAML.CharPredicates.isUriCharProp in `L4YAML/Spec/CharPredicates.lean:316` L4YAML.CharPredicates.isUriCharBool in `L4YAML/Spec/CharPredicates.lean:328`
40	ns-tag-char	§5.6	Covered			L4YAML.Scanner.collectTagSuffixLoop in `L4YAML/Scanner/NodeProperties.lean:102`	L4YAML.CharPredicates.isTagCharBool in `L4YAML/Spec/CharPredicates.lean:345` L4YAML.CharPredicates.isTagCharProp in `L4YAML/Spec/CharPredicates.lean:336`
41	c-escape	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`
42	ns-esc-null	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
43	ns-esc-bell	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
44	ns-esc-backspace	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
45	ns-esc-horizontal-tab	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218` L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42` L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
46	ns-esc-line-feed	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
47	ns-esc-vertical-tab	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
48	ns-esc-form-feed	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
49	ns-esc-carriage-return	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
50	ns-esc-escape	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42` L4YAML.Surface.SNbDoubleChar.hexEscape2 in `L4YAML/Surface/Scalars.lean:45`
51	ns-esc-space	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
52	ns-esc-double-quote	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
53	ns-esc-slash	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
54	ns-esc-backslash	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
55	ns-esc-next-line	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
56	ns-esc-non-breaking-space	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
57	ns-esc-line-separator	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
58	ns-esc-paragraph-separator	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`	L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42`
59	ns-esc-8-bit	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110` L4YAML.Scanner.parseHexEscape in `L4YAML/Scanner/Scalar.lean:71`
60	ns-esc-16-bit	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110` L4YAML.Scanner.parseHexEscape in `L4YAML/Scanner/Scalar.lean:71`		L4YAML.Surface.SNbDoubleChar.hexEscape4 in `L4YAML/Surface/Scalars.lean:48`
61	ns-esc-32-bit	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110` L4YAML.Scanner.parseHexEscape in `L4YAML/Scanner/Scalar.lean:71`		L4YAML.Surface.SNbDoubleChar.hexEscape8 in `L4YAML/Surface/Scalars.lean:52`
62	c-ns-esc-char	§5.7	Covered			L4YAML.Scanner.processEscape in `L4YAML/Scanner/Scalar.lean:110`	L4YAML.Grammar.resolveNamedEscape in `L4YAML/Spec/Grammar.lean:218`
63	s-indent(n)	§6.1	Covered			L4YAML.Scanner.skipSpaces in `L4YAML/Scanner/Whitespace.lean:101` L4YAML.Scanner.skipSpacesLoop in `L4YAML/Scanner/Whitespace.lean:88` L4YAML.Scanner.consumeExactSpaces in `L4YAML/Scanner/Scalar.lean:721` L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932` L4YAML.Scanner.skipSpacesLoop._unary in `L4YAML/Scanner/Whitespace.lean`	L4YAML.Grammar.Indented in `L4YAML/Spec/Grammar.lean:89`
64	s-indent(<n)	§6.1	Grammar Only			L4YAML.Scanner.unwindIndentsLoop._unary in `L4YAML/Scanner/Indent.lean` L4YAML.Scanner.unwindIndentsLoop in `L4YAML/Scanner/Indent.lean:41` L4YAML.Scanner.unwindIndents in `L4YAML/Scanner/Indent.lean:65`
65	s-indent(≤n)	§6.1	Grammar Only			L4YAML.Scanner.unwindIndentsLoop._unary in `L4YAML/Scanner/Indent.lean` L4YAML.Scanner.unwindIndentsLoop in `L4YAML/Scanner/Indent.lean:41` L4YAML.Scanner.unwindIndents in `L4YAML/Scanner/Indent.lean:65`	L4YAML.Grammar.IndentedAtLeast in `L4YAML/Spec/Grammar.lean:115`
66	s-separate-in-line	§6.2	Covered			L4YAML.Scanner.skipTrailingSpaces in `L4YAML/Scanner/Whitespace.lean:302` L4YAML.Scanner.skipWhitespaceLoop in `L4YAML/Scanner/Whitespace.lean:68` L4YAML.Scanner.skipDocEndWhitespace in `L4YAML/Scanner/Document.lean:291` L4YAML.Scanner.skipWhitespace in `L4YAML/Scanner/Whitespace.lean:81` L4YAML.Scanner.skipWhitespaceLoop._unary in `L4YAML/Scanner/Whitespace.lean`
67	s-line-prefix(n,c)	§6.3	Covered			L4YAML.Scanner.skipToContentWs in `L4YAML/Scanner/Whitespace.lean:154`
68	s-block-line-prefix(n)	§6.3	Covered			L4YAML.Scanner.skipToContentWs in `L4YAML/Scanner/Whitespace.lean:154`
69	s-flow-line-prefix(n)	§6.3	Covered			L4YAML.Scanner.foldQuotedNewlines in `L4YAML/Scanner/Scalar.lean:187`
70	l-empty(n,c)	§6.4	Covered			L4YAML.Scanner.skipBlankLinesLoop in `L4YAML/Scanner/Scalar.lean:393` L4YAML.Scanner.foldQuotedNewlinesLoop in `L4YAML/Scanner/Scalar.lean:153`
71	b-l-trimmed(n,c)	§6.5	Covered			L4YAML.Scanner.foldQuotedNewlines in `L4YAML/Scanner/Scalar.lean:187`
72	b-as-space	§6.5	Covered			L4YAML.Scanner.foldQuotedNewlines in `L4YAML/Scanner/Scalar.lean:187`
73	b-l-folded(n,c)	§6.5	Covered			L4YAML.Scanner.foldQuotedNewlines in `L4YAML/Scanner/Scalar.lean:187`
74	s-flow-folded(n)	§6.5	Covered			L4YAML.Scanner.foldQuotedNewlines in `L4YAML/Scanner/Scalar.lean:187`
75	c-nb-comment-text	§6.6	Covered			L4YAML.Scanner.scanBlockScalarSkipComment in `L4YAML/Scanner/Scalar.lean:820` L4YAML.Scanner.collectCommentTextLoop in `L4YAML/Scanner/Whitespace.lean:205` L4YAML.Scanner.scanWithComments in `L4YAML/Scanner/Scanner.lean:580` L4YAML.Scanner.collectCommentTextLoop._unary in `L4YAML/Scanner/Whitespace.lean` L4YAML.Scanner.skipToContentComment in `L4YAML/Scanner/Whitespace.lean:226`			L4YAML.YamlToken.comment in `L4YAML/Token/Token.lean:196`
76	b-comment	§6.6	Covered			L4YAML.Scanner.scanBlockScalarConsumeNewline in `L4YAML/Scanner/Scalar.lean:845`
77	s-b-comment	§6.6	Covered			L4YAML.Scanner.scanBlockScalarSkipComment in `L4YAML/Scanner/Scalar.lean:820` L4YAML.Scanner.skipToContentComment in `L4YAML/Scanner/Whitespace.lean:226`
78	l-comment	§6.7	Covered			L4YAML.Scanner.skipToContent in `L4YAML/Scanner/Whitespace.lean:295`
79	s-l-comments	§6.7	Covered			L4YAML.Scanner.skipToContentLoop in `L4YAML/Scanner/Whitespace.lean:251` L4YAML.Scanner.skipToContentLoop._unary in `L4YAML/Scanner/Whitespace.lean` L4YAML.Scanner.skipToContent in `L4YAML/Scanner/Whitespace.lean:295`
80	s-separate(n,c)	§6.7	Covered			L4YAML.Scanner.skipToContent in `L4YAML/Scanner/Whitespace.lean:295`
81	s-separate-lines(n)	§6.7	Covered			L4YAML.Scanner.skipToContent in `L4YAML/Scanner/Whitespace.lean:295`
82	l-directive	§6.8	Covered	L4YAML.TokenParser.parseDirectives in `L4YAML/Parser/TokenParser.lean:654`		L4YAML.Scanner.scanDirective in `L4YAML/Scanner/Document.lean:243` L4YAML.Scanner.scanNextToken_dispatchStructural in `L4YAML/Scanner/Scanner.lean:293`
83	ns-reserved-directive	§6.8	Covered			L4YAML.Scanner.scanDirective in `L4YAML/Scanner/Document.lean:243`
84	ns-directive-name	§6.8	Covered			L4YAML.Scanner.collectDirectiveNameLoop in `L4YAML/Scanner/Document.lean:87`
85	ns-directive-parameter	§6.8	Covered			L4YAML.Scanner.scanDirective in `L4YAML/Scanner/Document.lean:243`
86	ns-yaml-directive	§6.8.1	Covered			L4YAML.Scanner.scanYamlDirective in `L4YAML/Scanner/Document.lean:170`			L4YAML.YamlToken.versionDirective in `L4YAML/Token/Token.lean:113`
87	ns-yaml-version	§6.8.1	Covered			L4YAML.Scanner.scanYamlDirective in `L4YAML/Scanner/Document.lean:170` L4YAML.Scanner.collectVersionMajorLoop in `L4YAML/Scanner/Document.lean:102`
88	ns-tag-directive	§6.8.2	Covered			L4YAML.Scanner.scanTagDirective in `L4YAML/Scanner/Document.lean:200`			L4YAML.YamlToken.tagDirective in `L4YAML/Token/Token.lean:115`
89	c-tag-handle	§6.8.2	Covered			L4YAML.Scanner.scanTagDirective in `L4YAML/Scanner/Document.lean:200` L4YAML.Scanner.collectTagHandleDirectiveLoop in `L4YAML/Scanner/Document.lean:132`
90	c-primary-tag-handle	§6.8.2	Covered			L4YAML.Scanner.scanNamedTag in `L4YAML/Scanner/NodeProperties.lean:159`
91	c-secondary-tag-handle	§6.8.2	Covered			L4YAML.Scanner.scanSecondaryTag in `L4YAML/Scanner/NodeProperties.lean:147`
92	c-named-tag-handle	§6.8.2	Covered			L4YAML.Scanner.scanNamedTag in `L4YAML/Scanner/NodeProperties.lean:159`
93	ns-tag-prefix	§6.8.2	Covered			L4YAML.Scanner.scanTagDirective in `L4YAML/Scanner/Document.lean:200` L4YAML.Scanner.collectTagPrefixLoop in `L4YAML/Scanner/Document.lean:148`
94	c-ns-local-tag-prefix	§6.8.2	Covered			L4YAML.Scanner.collectTagPrefixLoop in `L4YAML/Scanner/Document.lean:148`
95	ns-global-tag-prefix	§6.8.2	Covered			L4YAML.Scanner.collectTagPrefixLoop in `L4YAML/Scanner/Document.lean:148`
96	c-ns-properties(n,c)	§6.9	Covered	L4YAML.TokenParser.parseNodeProperties in `L4YAML/Parser/State.lean:182`		L4YAML.Scanner.scanNextToken_dispatchContent in `L4YAML/Scanner/Scanner.lean:366`
97	c-ns-tag-property	§6.9	Covered			L4YAML.Scanner.scanTag in `L4YAML/Scanner/NodeProperties.lean:178`			L4YAML.YamlToken.tag in `L4YAML/Token/Token.lean:181`
98	c-verbatim-tag	§6.9	Covered			L4YAML.Scanner.scanVerbatimTag in `L4YAML/Scanner/NodeProperties.lean:133`
99	c-ns-shorthand-tag	§6.9	Covered	L4YAML.TokenParser.resolveTag in `L4YAML/Parser/State.lean:155`		L4YAML.Scanner.scanNamedTag in `L4YAML/Scanner/NodeProperties.lean:159` L4YAML.Scanner.scanSecondaryTag in `L4YAML/Scanner/NodeProperties.lean:147`
100	c-non-specific-tag	§6.9	Covered			L4YAML.Scanner.scanNamedTag in `L4YAML/Scanner/NodeProperties.lean:159`
101	c-ns-anchor-property	§6.9	Covered			L4YAML.Scanner.collectAnchorNameLoop in `L4YAML/Scanner/NodeProperties.lean:55` L4YAML.Scanner.scanAnchorOrAlias in `L4YAML/Scanner/NodeProperties.lean:69`			L4YAML.YamlToken.anchor in `L4YAML/Token/Token.lean:175`
102	ns-anchor-char	§6.9	Covered			L4YAML.Scanner.collectAnchorNameLoop in `L4YAML/Scanner/NodeProperties.lean:55`
103	ns-anchor-name	§6.9	Covered			L4YAML.Scanner.collectAnchorNameLoop in `L4YAML/Scanner/NodeProperties.lean:55`
104	c-ns-alias-node	§7.1	Covered			L4YAML.Scanner.collectAnchorNameLoop in `L4YAML/Scanner/NodeProperties.lean:55` L4YAML.Scanner.scanAnchorOrAlias in `L4YAML/Scanner/NodeProperties.lean:69`		L4YAML.Surface.SCNsAliasNode in `L4YAML/Surface/Scalars.lean:324`	L4YAML.YamlToken.alias in `L4YAML/Token/Token.lean:178`
105	e-scalar	§7.2	Covered	L4YAML.TokenParser.emptyNode in `L4YAML/Parser/State.lean:217`		L4YAML.Scanner.scanNextToken_dispatchContent in `L4YAML/Scanner/Scanner.lean:366`
106	e-node	§7.2	Covered	L4YAML.TokenParser.emptyNode in `L4YAML/Parser/State.lean:217`			L4YAML.Grammar.ValidNode.emptyNode in `L4YAML/Spec/Grammar.lean:313`
107	nb-double-char	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`		L4YAML.Surface.SNbDoubleChar in `L4YAML/Surface/Scalars.lean:38` L4YAML.Surface.SNbDoubleChar.plain in `L4YAML/Surface/Scalars.lean:39` L4YAML.Surface.SNbDoubleChar.hexEscape4 in `L4YAML/Surface/Scalars.lean:48` L4YAML.Surface.SNbDoubleChar.escape in `L4YAML/Surface/Scalars.lean:42` L4YAML.Surface.SNbDoubleChar.hexEscape2 in `L4YAML/Surface/Scalars.lean:45` L4YAML.Surface.SNbDoubleChar.hexEscape8 in `L4YAML/Surface/Scalars.lean:52`
108	ns-double-char	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`
109	c-double-quoted(n,c)	§7.3.1	Covered		L4YAML.Proofs.NodeProduction.SCDoubleQuoted_ctx_lift in `L4YAML/Proofs/Production/NodeProduction.lean:249`	L4YAML.Scanner.scanDoubleQuoted in `L4YAML/Scanner/Scalar.lean:297`	L4YAML.Grammar.ValidNode.doubleQuoted in `L4YAML/Spec/Grammar.lean:297` L4YAML.Grammar.ValidNode.doubleQuoted in `L4YAML/Spec/Grammar.lean:297`	L4YAML.Surface.SCDoubleQuoted in `L4YAML/Surface/Scalars.lean:156`	L4YAML.YamlToken.scalar in `L4YAML/Token/Token.lean:190`
110	nb-double-text(n,c)	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`		L4YAML.Surface.SNbDoubleText in `L4YAML/Surface/Scalars.lean:148`
111	nb-double-one-line	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`		L4YAML.Surface.SNbDoubleOneLine in `L4YAML/Surface/Scalars.lean:130`
112	s-double-escaped(n)	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`		L4YAML.Surface.SSDoubleEscaped in `L4YAML/Surface/Scalars.lean:107`
113	s-double-break(n)	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`		L4YAML.Surface.SSDoubleBreak in `L4YAML/Surface/Scalars.lean:119`
114	nb-ns-double-in-line	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`
115	s-double-next-line(n)	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`
116	nb-double-multi-line(n)	§7.3.1	Covered			L4YAML.Scanner.collectDoubleQuotedLoop in `L4YAML/Scanner/Scalar.lean:229`		L4YAML.Surface.SNbDoubleMultiLine in `L4YAML/Surface/Scalars.lean:134`
117	c-quoted-quote	§7.3.2	Covered			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318`
118	nb-single-char	§7.3.2	Covered			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318`		L4YAML.Surface.SNbSingleChar in `L4YAML/Surface/Scalars.lean:168`
119	ns-single-char	§7.3.2	Covered			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318`
120	c-single-quoted(n,c)	§7.3.2	Covered		L4YAML.Proofs.NodeProduction.SCSingleQuoted_ctx_lift in `L4YAML/Proofs/Production/NodeProduction.lean:268`	L4YAML.Scanner.scanSingleQuoted in `L4YAML/Scanner/Scalar.lean:374`	L4YAML.Grammar.ValidNode.singleQuoted in `L4YAML/Spec/Grammar.lean:295` L4YAML.Grammar.ValidNode.singleQuoted in `L4YAML/Spec/Grammar.lean:295`	L4YAML.Surface.SCSingleQuoted in `L4YAML/Surface/Scalars.lean:205`	L4YAML.YamlToken.scalar in `L4YAML/Token/Token.lean:190`
121	nb-single-text(n,c)	§7.3.2	Covered			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318`		L4YAML.Surface.SNbSingleText in `L4YAML/Surface/Scalars.lean:197`
122	nb-single-one-line	§7.3.2	Covered			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318`		L4YAML.Surface.SNbSingleOneLine in `L4YAML/Surface/Scalars.lean:177`
123	nb-ns-single-in-line	§7.3.2	Covered			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318`
124	s-single-next-line(n)	§7.3.2	Covered			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318`
125	nb-single-multi-line(n)	§7.3.2	Covered			L4YAML.Scanner.collectSingleQuotedLoop in `L4YAML/Scanner/Scalar.lean:318`		L4YAML.Surface.SNbSingleMultiLine in `L4YAML/Surface/Scalars.lean:181`
126	ns-plain-first(c)	§7.3.3	Covered			L4YAML.Scanner.collectPlainScalar_terminates? in `L4YAML/Scanner/Scalar.lean:427`	L4YAML.CharPredicates.canStartPlainScalarBool in `L4YAML/Spec/CharPredicates.lean:365` L4YAML.CharPredicates.canStartPlainScalarProp in `L4YAML/Spec/CharPredicates.lean:379` L4YAML.CharPredicates.validPlainFirstProp in `L4YAML/Spec/CharPredicates.lean:521` L4YAML.CharPredicates.validPlainFirstBool in `L4YAML/Spec/CharPredicates.lean:503`	L4YAML.Surface.SNsPlainFirst in `L4YAML/Surface/Scalars.lean:227`
127	ns-plain-safe(c)	§7.3.3	Covered				L4YAML.CharPredicates.isPlainSafeBool in `L4YAML/Spec/CharPredicates.lean:446` L4YAML.CharPredicates.isPlainSafeProp in `L4YAML/Spec/CharPredicates.lean:461` L4YAML.CharPredicates.noFlowIndicatorsProp in `L4YAML/Spec/CharPredicates.lean:769` L4YAML.CharPredicates.noFlowIndicatorsBool in `L4YAML/Spec/CharPredicates.lean:764`	L4YAML.Surface.isNsPlainSafe in `L4YAML/Surface/Scalars.lean:217`
128	ns-plain-safe-out	§7.3.3	Covered				L4YAML.CharPredicates.isPlainSafeBool in `L4YAML/Spec/CharPredicates.lean:446` L4YAML.CharPredicates.isPlainSafeProp in `L4YAML/Spec/CharPredicates.lean:461`
129	ns-plain-safe-in	§7.3.3	Covered			L4YAML.Scanner.collectPlainScalar_terminates? in `L4YAML/Scanner/Scalar.lean:427`	L4YAML.CharPredicates.isPlainSafeBool in `L4YAML/Spec/CharPredicates.lean:446` L4YAML.CharPredicates.isPlainSafeProp in `L4YAML/Spec/CharPredicates.lean:461`
130	ns-plain-char(c)	§7.3.3	Covered				L4YAML.CharPredicates.noSpaceHashBool in `L4YAML/Spec/CharPredicates.lean:737` L4YAML.CharPredicates.noColonSpaceBool in `L4YAML/Spec/CharPredicates.lean:710` L4YAML.CharPredicates.noSpaceHashProp in `L4YAML/Spec/CharPredicates.lean:742` L4YAML.CharPredicates.noColonSpaceProp in `L4YAML/Spec/CharPredicates.lean:715`	L4YAML.Surface.SNsPlainChar in `L4YAML/Surface/Scalars.lean:244`
131	ns-plain(n,c)	§7.3.3	Covered			L4YAML.Scanner.collectPlainScalar_terminates? in `L4YAML/Scanner/Scalar.lean:427` L4YAML.Scanner.scanPlainScalar in `L4YAML/Scanner/Scalar.lean:555`	L4YAML.Grammar.ValidNode.plainScalarFlow in `L4YAML/Spec/Grammar.lean:290` L4YAML.Grammar.ValidNode.plainScalarBlock in `L4YAML/Spec/Grammar.lean:285`	L4YAML.Surface.SNsPlain in `L4YAML/Surface/Scalars.lean:314`	L4YAML.YamlToken.scalar in `L4YAML/Token/Token.lean:190`
132	nb-ns-plain-in-line(c)	§7.3.3	Covered			L4YAML.Scanner.collectPlainScalarLoop in `L4YAML/Scanner/Scalar.lean:480`		L4YAML.Surface.SNbNsPlainInLineEntry in `L4YAML/Surface/Scalars.lean:263`
133	ns-plain-one-line(c)	§7.3.3	Covered			L4YAML.Scanner.collectPlainScalarLoop in `L4YAML/Scanner/Scalar.lean:480`		L4YAML.Surface.SNsPlainOneLine in `L4YAML/Surface/Scalars.lean:273`
134	s-ns-plain-next-line(n,c)	§7.3.3	Covered			L4YAML.Scanner.collectPlainScalarLoop in `L4YAML/Scanner/Scalar.lean:480` L4YAML.Scanner.collectPlainScalar_handleBlockLineBreak in `L4YAML/Scanner/Scalar.lean:457`		L4YAML.Surface.SSNsPlainNextLine in `L4YAML/Surface/Scalars.lean:291`
135	ns-plain-multi-line(n,c)	§7.3.3	Covered			L4YAML.Scanner.collectPlainScalarLoop in `L4YAML/Scanner/Scalar.lean:480` L4YAML.Scanner.collectPlainScalar_handleBlockLineBreak in `L4YAML/Scanner/Scalar.lean:457`		L4YAML.Surface.SNsPlainMultiLine in `L4YAML/Surface/Scalars.lean:302`
136	in-flow(c)	§7.4	Covered			L4YAML.Scanner.ScannerState.inFlow in `L4YAML/Scanner/State.lean:243`
137	c-flow-sequence(n,c)	§7.4.1	Covered	L4YAML.TokenParser.parseFlowSequence in `L4YAML/Parser/TokenParser.lean:387`		L4YAML.Scanner.scanFlowSequenceStart in `L4YAML/Scanner/Scanner.lean:134` L4YAML.Scanner.scanNextToken_dispatchFlowIndicators in `L4YAML/Scanner/Scanner.lean:319`	L4YAML.Grammar.ValidNode.flowSeq in `L4YAML/Spec/Grammar.lean:307` L4YAML.Grammar.ValidNode.flowSeq in `L4YAML/Spec/Grammar.lean:307`	L4YAML.Surface.SFlowSequence in `L4YAML/Surface/Node.lean:291`
138	ns-s-flow-seq-entries(n,c)	§7.4.1	Covered	L4YAML.TokenParser.parseFlowSequenceLoop in `L4YAML/Parser/TokenParser.lean:400`				L4YAML.Surface.SFlowSeqEntries in `L4YAML/Surface/Node.lean:306`
139	ns-flow-seq-entry(n,c)	§7.4.1	Covered	L4YAML.TokenParser.parseFlowSequenceLoop in `L4YAML/Parser/TokenParser.lean:400`				L4YAML.Surface.SFlowSeqEntry in `L4YAML/Surface/Node.lean:327`
140	c-flow-mapping(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseFlowMapping in `L4YAML/Parser/TokenParser.lean:445`		L4YAML.Scanner.scanFlowMappingStart in `L4YAML/Scanner/Scanner.lean:185` L4YAML.Scanner.scanNextToken_dispatchFlowIndicators in `L4YAML/Scanner/Scanner.lean:319`	L4YAML.Grammar.ValidNode.flowMap in `L4YAML/Spec/Grammar.lean:309`	L4YAML.Surface.SFlowMapping in `L4YAML/Surface/Node.lean:349`
141	ns-s-flow-map-entries(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseFlowMappingLoop in `L4YAML/Parser/TokenParser.lean:495`				L4YAML.Surface.SFlowMapEntries in `L4YAML/Surface/Node.lean:364`
142	ns-flow-map-entry(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseFlowMappingLoop in `L4YAML/Parser/TokenParser.lean:495`				L4YAML.Surface.SFlowMapEntry in `L4YAML/Surface/Node.lean:385`
143	ns-flow-map-explicit-entry(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseExplicitKey in `L4YAML/Parser/TokenParser.lean:481`
144	ns-flow-map-implicit-entry(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseFlowMappingLoop in `L4YAML/Parser/TokenParser.lean:495`
145	ns-flow-map-yaml-key-entry(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseFlowMappingLoop in `L4YAML/Parser/TokenParser.lean:495`
146	c-ns-flow-map-empty-key-entry(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseFlowMappingLoop in `L4YAML/Parser/TokenParser.lean:495`
147	c-ns-flow-map-separate-value(n,c)	§7.4.2	Covered			L4YAML.Scanner.isValueCandidate in `L4YAML/Scanner/SimpleKey.lean:303`
148	c-ns-flow-map-json-key-entry(n,c)	§7.4.2	Covered			L4YAML.Scanner.isValueCandidate in `L4YAML/Scanner/SimpleKey.lean:303`
149	c-ns-flow-map-adjacent-value(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseFlowMappingValue in `L4YAML/Parser/TokenParser.lean:459`
150	ns-flow-pair(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseSinglePairMapping in `L4YAML/Parser/TokenParser.lean:536`
151	ns-flow-pair-entry(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseSinglePairMapping in `L4YAML/Parser/TokenParser.lean:536`
152	ns-flow-pair-yaml-key-entry(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseSinglePairMapping in `L4YAML/Parser/TokenParser.lean:536`
153	c-ns-flow-pair-json-key-entry(n,c)	§7.4.2	Covered	L4YAML.TokenParser.parseSinglePairMapping in `L4YAML/Parser/TokenParser.lean:536`
154	ns-s-implicit-yaml-key(c)	§7.4.2	Covered			L4YAML.Scanner.saveSimpleKey in `L4YAML/Scanner/SimpleKey.lean:246`
155	c-s-implicit-json-key(c)	§7.4.2	Covered	L4YAML.TokenParser.parseFlowMappingLoop in `L4YAML/Parser/TokenParser.lean:495`
156	ns-flow-yaml-content(n,c)	§7.5	Covered	L4YAML.TokenParser.parseNodeContent._mutual in `L4YAML/Parser/TokenParser.lean` L4YAML.TokenParser.parseNodeContent in `L4YAML/Parser/TokenParser.lean:92`
157	c-flow-json-content(n,c)	§7.5	Covered	L4YAML.TokenParser.parseNodeContent._mutual in `L4YAML/Parser/TokenParser.lean` L4YAML.TokenParser.parseNodeContent in `L4YAML/Parser/TokenParser.lean:92`
158	ns-flow-content(n,c)	§7.5	Covered	L4YAML.TokenParser.parseNodeContent._mutual in `L4YAML/Parser/TokenParser.lean` L4YAML.TokenParser.parseNodeContent in `L4YAML/Parser/TokenParser.lean:92`				L4YAML.Surface.SFlowContent in `L4YAML/Surface/Node.lean:267`
159	ns-flow-yaml-node(n,c)	§7.5	Covered	L4YAML.TokenParser.parseNodeContent._mutual in `L4YAML/Parser/TokenParser.lean` L4YAML.TokenParser.parseNodeContent in `L4YAML/Parser/TokenParser.lean:92`
160	c-flow-json-node(n,c)	§7.5	Covered			L4YAML.Scanner.isJsonNodeToken in `L4YAML/Scanner/SimpleKey.lean:287`
161	ns-flow-node(n,c)	§7.5	Covered	L4YAML.TokenParser.parseNode in `L4YAML/Parser/TokenParser.lean:131`		L4YAML.Scanner.scanNextToken_dispatchContent in `L4YAML/Scanner/Scanner.lean:366`	L4YAML.Grammar.ValidNode in `L4YAML/Spec/Grammar.lean:281`	L4YAML.Surface.SFlowNode in `L4YAML/Surface/Node.lean:245`
162	c-b-block-header(t)	§8.1.1	Covered			L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932` L4YAML.Scanner.parseBlockHeaderLoop in `L4YAML/Scanner/Scalar.lean:796`	L4YAML.Grammar.isBlockScalarHeaderChar in `L4YAML/Spec/Grammar.lean:792`	L4YAML.Surface.SCBBlockHeader in `L4YAML/Surface/Scalars.lean:339`
163	c-indentation-indicator	§8.1.1	Covered			L4YAML.Scanner.autoDetectBlockScalarIndentLoop in `L4YAML/Scanner/Scalar.lean:674` L4YAML.Scanner.autoDetectBlockScalarIndent in `L4YAML/Scanner/Scalar.lean:713` L4YAML.Scanner.scanBlockScalarBody in `L4YAML/Scanner/Scalar.lean:875` L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932`	L4YAML.Grammar.isBlockScalarHeaderChar in `L4YAML/Spec/Grammar.lean:792`
164	c-chomping-indicator(t)	§8.1.1	Covered			L4YAML.Scanner.scanBlockScalarBody in `L4YAML/Scanner/Scalar.lean:875` L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932`	L4YAML.Grammar.isBlockScalarHeaderChar in `L4YAML/Spec/Grammar.lean:792`
165	b-chomped-last(t)	§8.1.1	Covered			L4YAML.Scanner.scanBlockScalarBody in `L4YAML/Scanner/Scalar.lean:875`
166	l-chomped-empty(n,t)	§8.1.1	Covered			L4YAML.Scanner.scanBlockScalarBody in `L4YAML/Scanner/Scalar.lean:875`
167	l-strip-empty(n)	§8.1.1	Covered			L4YAML.Scanner.scanBlockScalarBody in `L4YAML/Scanner/Scalar.lean:875`
168	l-keep-empty(n)	§8.1.1	Covered			L4YAML.Scanner.scanBlockScalarBody in `L4YAML/Scanner/Scalar.lean:875`
169	l-trail-comments(n)	§8.1.1	Covered			L4YAML.Scanner.scanBlockScalarBody in `L4YAML/Scanner/Scalar.lean:875`
170	c-l+literal(n)	§8.1.2	Covered			L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932`	L4YAML.Grammar.ValidNode.literalScalar in `L4YAML/Spec/Grammar.lean:299` L4YAML.Grammar.ValidNode.literalScalar in `L4YAML/Spec/Grammar.lean:299`	L4YAML.Surface.SCLLiteral in `L4YAML/Surface/Scalars.lean:378`	L4YAML.YamlToken.scalar in `L4YAML/Token/Token.lean:190`
171	l-nb-literal-text(n)	§8.1.2	Covered			L4YAML.Scanner.scanBlockScalarBody in `L4YAML/Scanner/Scalar.lean:875` L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932` L4YAML.Scanner.collectLineContentLoop in `L4YAML/Scanner/Scalar.lean:734`		L4YAML.Surface.SLNbLiteralText in `L4YAML/Surface/Scalars.lean:348`
172	b-nb-literal-next(n)	§8.1.2	Covered			L4YAML.Scanner.collectBlockScalarLoop in `L4YAML/Scanner/Scalar.lean:750` L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932`		L4YAML.Surface.SBNbLiteralNext in `L4YAML/Surface/Scalars.lean:356`
173	l-literal-content(n,t)	§8.1.2	Covered			L4YAML.Scanner.collectBlockScalarLoop in `L4YAML/Scanner/Scalar.lean:750` L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932`		L4YAML.Surface.SLLiteralContent in `L4YAML/Surface/Scalars.lean:365`
174	c-l+folded(n)	§8.1.3	Covered			L4YAML.Scanner.scanBlockScalar in `L4YAML/Scanner/Scalar.lean:932` L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`	L4YAML.Grammar.ValidNode.foldedScalar in `L4YAML/Spec/Grammar.lean:301` L4YAML.Grammar.ValidNode.foldedScalar in `L4YAML/Spec/Grammar.lean:301`	L4YAML.Surface.SCLFolded in `L4YAML/Surface/Scalars.lean:408`	L4YAML.YamlToken.scalar in `L4YAML/Token/Token.lean:190`
175	s-nb-folded-text(n)	§8.1.3	Covered			L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`		L4YAML.Surface.SSNbFoldedText in `L4YAML/Surface/Scalars.lean:386`
176	l-nb-folded-lines(n)	§8.1.3	Covered			L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`		L4YAML.Surface.SLNbFoldedLines in `L4YAML/Surface/Scalars.lean:393`
177	s-nb-spaced-text(n)	§8.1.3	Covered			L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`
178	b-l-spaced(n)	§8.1.3	Covered			L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`
179	l-nb-spaced-lines(n)	§8.1.3	Covered			L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`
180	l-nb-same-lines(n)	§8.1.3	Covered			L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`
181	l-nb-diff-lines(n)	§8.1.3	Covered			L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`
182	l-folded-content(n,t)	§8.1.3	Covered			L4YAML.Scanner.foldBlockContent in `L4YAML/Scanner/Scalar.lean:620`
183	l+block-sequence(n)	§8.2.1	Covered	L4YAML.TokenParser.parseBlockSequence in `L4YAML/Parser/TokenParser.lean:172`		L4YAML.Scanner.pushSequenceIndent in `L4YAML/Scanner/Indent.lean:76`	L4YAML.Grammar.ValidNode.blockSeq in `L4YAML/Spec/Grammar.lean:303` L4YAML.Grammar.ValidNode.blockSeq in `L4YAML/Spec/Grammar.lean:303`	L4YAML.Surface.SBlockSeqEntries in `L4YAML/Surface/Node.lean:127`
184	c-l-block-seq-entry(n)	§8.2.1	Covered	L4YAML.TokenParser.parseBlockSequenceLoop in `L4YAML/Parser/TokenParser.lean:185`		L4YAML.Scanner.isBlockEntryCandidate in `L4YAML/Scanner/SimpleKey.lean:269` L4YAML.Scanner.scanBlockEntry in `L4YAML/Scanner/SimpleKey.lean:63` L4YAML.Scanner.scanNextToken_dispatchBlockIndicators in `L4YAML/Scanner/Scanner.lean:346`
185	s-l+block-indented(n,c)	§8.2.1	Covered	L4YAML.TokenParser.parseNode in `L4YAML/Parser/TokenParser.lean:131`				L4YAML.Surface.SBlockIndented in `L4YAML/Surface/Node.lean:102`
186	ns-l-compact-sequence(n)	§8.2.1	Covered	L4YAML.TokenParser.parseImplicitBlockSequence in `L4YAML/Parser/TokenParser.lean:220`				L4YAML.Surface.SCompactSeq in `L4YAML/Surface/Node.lean:191`
187	l+block-mapping(n)	§8.2.2	Covered	L4YAML.TokenParser.parseBlockMapping in `L4YAML/Parser/TokenParser.lean:265`		L4YAML.Scanner.pushMappingIndent in `L4YAML/Scanner/Indent.lean:90`	L4YAML.Grammar.ValidNode.blockMap in `L4YAML/Spec/Grammar.lean:305` L4YAML.Grammar.ValidNode.blockMap in `L4YAML/Spec/Grammar.lean:305`	L4YAML.Surface.SBlockMapEntries in `L4YAML/Surface/Node.lean:178`
188	ns-l-block-map-entry(n)	§8.2.2	Covered	L4YAML.TokenParser.parseBlockMappingEntryValue in `L4YAML/Parser/TokenParser.lean:280`				L4YAML.Surface.SBlockMapEntry in `L4YAML/Surface/Node.lean:144`
189	c-l-block-map-explicit-entry(n)	§8.2.2	Covered	L4YAML.TokenParser.handleBlockMappingKeyEntry in `L4YAML/Parser/TokenParser.lean:316`
190	c-l-block-map-explicit-key(n)	§8.2.2	Covered	L4YAML.TokenParser.handleBlockMappingKeyEntry in `L4YAML/Parser/TokenParser.lean:316`		L4YAML.Scanner.scanKey in `L4YAML/Scanner/SimpleKey.lean:93` L4YAML.Scanner.scanNextToken_dispatchBlockIndicators in `L4YAML/Scanner/Scanner.lean:346`
191	l-block-map-explicit-value(n)	§8.2.2	Covered	L4YAML.TokenParser.handleBlockMappingValueEntry in `L4YAML/Parser/TokenParser.lean:344`		L4YAML.Scanner.isKeyCandidate in `L4YAML/Scanner/SimpleKey.lean:277`
192	ns-l-block-map-implicit-entry(n)	§8.2.2	Covered	L4YAML.TokenParser.parseBlockMappingLoop in `L4YAML/Parser/TokenParser.lean:360`
193	ns-s-block-map-implicit-key	§8.2.2	Covered	L4YAML.TokenParser.handleBlockMappingKeyEntry in `L4YAML/Parser/TokenParser.lean:316`				L4YAML.Surface.SImplicitKey in `L4YAML/Surface/Node.lean:230`
194	c-l-block-map-implicit-value(n)	§8.2.2	Covered	L4YAML.TokenParser.handleBlockMappingValueEntry in `L4YAML/Parser/TokenParser.lean:344`
195	ns-l-compact-mapping(n)	§8.2.2	Covered	L4YAML.TokenParser.parseBlockMappingLoop in `L4YAML/Parser/TokenParser.lean:360`				L4YAML.Surface.SCompactMap in `L4YAML/Surface/Node.lean:212`
196	s-l+block-node(n,c)	§8.2.3	Covered	L4YAML.TokenParser.parseNode in `L4YAML/Parser/TokenParser.lean:131`			L4YAML.Grammar.ValidNode in `L4YAML/Spec/Grammar.lean:281`	L4YAML.Surface.SBlockNode in `L4YAML/Surface/Node.lean:62`
197	s-l+flow-in-block(n)	§8.2.3	Covered	L4YAML.TokenParser.parseNode in `L4YAML/Parser/TokenParser.lean:131`
198	s-l+block-in-block(n,c)	§8.2.3	Covered	L4YAML.TokenParser.parseNode in `L4YAML/Parser/TokenParser.lean:131`
199	s-l+block-scalar(n,c)	§8.2.3	Covered	L4YAML.TokenParser.parseNode in `L4YAML/Parser/TokenParser.lean:131`
200	s-l+block-collection(n,c)	§8.2.3	Covered	L4YAML.TokenParser.parseNode in `L4YAML/Parser/TokenParser.lean:131`
201	seq-space(n,c)	§8.2.1	Covered	L4YAML.TokenParser.parseNode in `L4YAML/Parser/TokenParser.lean:131`
202	l-document-prefix	§9.1.1	Covered	L4YAML.TokenParser.prepareDocumentState in `L4YAML/Parser/TokenParser.lean:675`		L4YAML.Scanner.scan in `L4YAML/Scanner/Scanner.lean:524`		L4YAML.Surface.SLDocumentPrefix in `L4YAML/Surface/Document.lean:118`
203	c-directives-end	§9.1.2	Covered			L4YAML.Scanner.atDocumentStart in `L4YAML/Scanner/Document.lean:45` L4YAML.Scanner.scanNextToken_dispatchStructural in `L4YAML/Scanner/Scanner.lean:293` L4YAML.Scanner.scanDocumentStart in `L4YAML/Scanner/Document.lean:275`		L4YAML.Surface.SCDirectivesEnd in `L4YAML/Surface/Document.lean:52`	L4YAML.YamlToken.documentStart in `L4YAML/Token/Token.lean:120`
204	c-document-end	§9.1.2	Covered			L4YAML.Scanner.scanDocumentEnd in `L4YAML/Scanner/Document.lean:314` L4YAML.Scanner.atDocumentEnd in `L4YAML/Scanner/Document.lean:64` L4YAML.Scanner.scanNextToken_dispatchStructural in `L4YAML/Scanner/Scanner.lean:293`		L4YAML.Surface.SCDocumentEnd in `L4YAML/Surface/Document.lean:59`	L4YAML.YamlToken.documentEnd in `L4YAML/Token/Token.lean:122`
205	l-document-suffix	§9.1.2	Covered			L4YAML.Scanner.scanDocumentEnd in `L4YAML/Scanner/Document.lean:314`		L4YAML.Surface.SLDocumentSuffix in `L4YAML/Surface/Document.lean:127`
206	c-forbidden	§9.1.2	Covered			L4YAML.Scanner.atDocumentBoundary in `L4YAML/Scanner/Document.lean:79`	L4YAML.Grammar.isCForbiddenPrefix in `L4YAML/Spec/Grammar.lean:164`	L4YAML.Surface.SCForbidden in `L4YAML/Surface/Document.lean:41`
207	l-bare-document	§9.1.3	Covered	L4YAML.TokenParser.parseDocument in `L4YAML/Parser/TokenParser.lean:713`			L4YAML.Grammar.ValidDocument in `L4YAML/Spec/Grammar.lean:354`	L4YAML.Surface.SLBareDocument in `L4YAML/Surface/Document.lean:71`
208	l-explicit-document	§9.1.4	Covered	L4YAML.TokenParser.parseDocument in `L4YAML/Parser/TokenParser.lean:713`			L4YAML.Grammar.ValidDocument in `L4YAML/Spec/Grammar.lean:354`	L4YAML.Surface.SLExplicitDocument in `L4YAML/Surface/Document.lean:79`
209	l-directive-document	§9.1.5	Covered	L4YAML.TokenParser.parseDocument in `L4YAML/Parser/TokenParser.lean:713`			L4YAML.Grammar.ValidDocument in `L4YAML/Spec/Grammar.lean:354`	L4YAML.Surface.SLDirectiveDocument in `L4YAML/Surface/Document.lean:88`
210	l-any-document	§9.2	Covered	L4YAML.TokenParser.parseDocument in `L4YAML/Parser/TokenParser.lean:713`			L4YAML.Grammar.ValidDocument in `L4YAML/Spec/Grammar.lean:354`	L4YAML.Surface.SLAnyDocument in `L4YAML/Surface/Document.lean:96`
211	l-yaml-stream	§9.2	Covered	L4YAML.TokenParser.parseStream in `L4YAML/Parser/TokenParser.lean:784` L4YAML.TokenParser.StreamState.validNextToken in `L4YAML/Parser/TokenParser.lean:609`		L4YAML.Scanner.scan in `L4YAML/Scanner/Scanner.lean:524` L4YAML.Scanner.scanFiltered in `L4YAML/Scanner/Scanner.lean:538` L4YAML.Scanner.scanLoopFull in `L4YAML/Scanner/Scanner.lean:546` L4YAML.Scanner.scanLoopFull._unary in `L4YAML/Scanner/Scanner.lean` L4YAML.Scanner.scanWithComments in `L4YAML/Scanner/Scanner.lean:580` L4YAML.Scanner.scanNextToken_preprocess in `L4YAML/Scanner/Scanner.lean:270`	L4YAML.Grammar.ValidStream in `L4YAML/Spec/Grammar.lean:371`	L4YAML.Surface.SLYamlStream in `L4YAML/Surface/Document.lean:136`

Auto-generated by @[yaml_spec] environment query · lean4-yaml-verified · Lean 4