mk

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Sat.Valuation.mk

Lean4

/-- `Valuation.mk [a, b, c]` is a valuation which is `a` at 0, `b` at 1 and `c` at 2, and false
everywhere else. -/
def mk : List Prop → Valuation
  | [], _ => False
  | a :: _, 0 => a
  | _ :: as, n + 1 => mk as n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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