Theory Interval_Point_Digest

theory Interval_Point_Digest
  imports Interval_Domain
begin

section ‹Interval point abstraction›

text ‹The point abstraction maps an integer to its singleton interval.›

definition ivl_decode :: "Int.int ⇒ ivl" where
  "ivl_decode v = Ivl (Fin v) (Fin v)"

end