Mathlib Map

Theorems · Definition · computer science

ContextFreeGrammar.NT

{T : Type u_1} → ContextFreeGrammar T → Type

Type of nonterminals.

Defined in
Mathlib.Computability.ContextFreeGrammar
Cited by
30 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ContextFreeGrammar.Derives · cited by 19ContextFreeGrammar.DerivesContextFreeGrammar.reverse · cited by 19ContextFreeGrammar.reverseContextFreeGrammar.Produces · cited by 17ContextFreeGrammar.Produc…ContextFreeGrammar.rules · cited by 9ContextFreeGrammar.rulesContextFreeGrammar.initial · cited by 7ContextFreeGrammar.initialContextFreeGrammar.Derives.trans_produces · cited by 3Derives.trans_producesContextFreeGrammar.Generates · cited by 3ContextFreeGrammar.Genera…ContextFreeGrammar.Derives.trans · cited by 2Derives.transContextFreeGrammar.Produces.single · cited by 2Produces.singleContextFreeGrammar.reverse_reverse · cited by 2ContextFreeGrammar.revers…ContextFreeGrammar.Derives.reverse · cited by 1Derives.reverseContextFreeGrammar.Produces.append_left · cited by 1Produces.append_leftContextFreeGrammar.Produces.append_right · cited by 1Produces.append_rightContextFreeGrammar.Produces.exists_nonterminal_input_mem · cited by 1Produces.exists_nontermin…ContextFreeGrammar.Produces.reverse · cited by 1Produces.reverseContextFreeGrammar · cited by 39ContextFreeGrammarContextFreeGrammar.NTCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by36

Results whose statement or proof uses this declaration.