Mathlib Map

Theorems · Inductive type · computer science

Symbol

Type u_4 → Type u_5 → Type (max u_4 u_5)

Symbols for use by all kinds of grammars.

Defined in
Mathlib.Computability.Language
Cited by
47 results in Mathlib
Foundations
Depth 0 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.Produces · cited by 17ContextFreeGrammar.Produc…ContextFreeRule.Rewrites · cited by 16ContextFreeRule.RewritesContextFreeRule.output · cited by 10ContextFreeRule.outputContextFreeGrammar.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.singleContextFreeRule.Rewrites.append_left · cited by 2Rewrites.append_leftContextFreeRule.Rewrites.append_right · cited by 2Rewrites.append_rightContextFreeRule.Rewrites.below · cited by 2Rewrites.belowContextFreeRule.rewrites_iff · cited by 2ContextFreeRule.rewrites_…ContextFreeGrammar.Derives.reverse · cited by 1Derives.reverseContextFreeGrammar.Produces.append_left · cited by 1Produces.append_leftContextFreeGrammar.Produces.append_right · cited by 1Produces.append_rightSymbolCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by73

Results whose statement or proof uses this declaration.