instMembershipPFun

Mathlib.Computability.PartrecCode

URI: https://scilib.ai/kg/mathlib#Nat.Partrec.Code.instMembershipPFun

English

Code is a member of the type of partial functions, via eval: Code is a mapping to PFun Nat Nat.

Русский

Код является элементом типа частичных функций через отображение eval: Code → Nat → Nat.

LaTeX

$$$\\text{Membership} (\\mathbb{N} \\to^. \\mathbb{N})\\; \\mathrm{Code}$$$

Lean4

instance : Membership (ℕ →. ℕ) Code :=
  ⟨fun c f => eval c = f⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru