ofInt

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Sat.Literal.ofInt

Lean4

/-- Construct a literal. Positive numbers are translated to positive literals,
  and negative numbers become negative literals. The input is assumed to be nonzero. -/
def ofInt (i : Int) : Literal :=
  if i < 0 then Literal.neg (-i - 1).toNat else Literal.pos (i - 1).toNat

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

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

Разделы

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

Аффилиация

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