opaque DUnif.oracleInstOn : Lean.Option Bool

def DUnif.getOracleInstOn : Lean.CoreM Bool

Equations

• DUnif.getOracleInstOn = do let opts ← Lean.getOptions pure (Lean.Option.get opts DUnif.oracleInstOn)

def DUnif.oracleInst (p : UnifProblem) (eq : UnifEq) : Lean.MetaM (Option UnifProblem)

Equations

• One or more equations did not get rendered due to their size.

opaque DUnif.oracleOccursOn : Lean.Option Bool

def DUnif.getOracleOccursOn : Lean.CoreM Bool

Equations

• DUnif.getOracleOccursOn = do let opts ← Lean.getOptions pure (Lean.Option.get opts DUnif.oracleOccursOn)

def DUnif.oracleOccurs (p : UnifProblem) (eq : UnifEq) : Lean.MetaM Bool

Equations

• One or more equations did not get rendered due to their size.