Binary splitting of intervals

This file defines the inclusion parameter binSplit for binary splitting of intervals, and a shared expression builder mkBinarySplitCover for constructing the binary-splitting cover in Interval expressions.

def Inclusion.Interval.binarySplitParam : InclusionParamDecl

The maximum depth of binary splitting of bounded intervals.

Equations

• Inclusion.Interval.binarySplitParam = { name := `binSplit, type := q(ℕ) }

@[inline]

def Inclusion.Interval.mkBinarySplitCover {u v : Lean.Level} {Iα : Q(Type u)} {α : Q(Type v)} {inst : Q(ToSet «$Iα» «$α»)} (cover : Q(ℕ → Cover «$Iα» «$α»)) : InclusionM (Option Lean.Expr)

Construct the binary-splitting cover from the binSplit parameter. If binSplit is omitted, return none. Otherwise, for binSplit := n, return some of the expression cover n.

Equations

• Inclusion.Interval.mkBinarySplitCover cover = do let __do_lift ← Inclusion.InclusionM.getParam? `binSplit pure (Option.map (Lean.mkApp cover) __do_lift)