IamExplainer.Condition

CondWarning — ⚪ definition

structure · source

structure CondWarning where

CondKeyVal — ⚪ definition

structure · source

structure CondKeyVal where

CondOp — ⚪ definition

structure · source

structure CondOp where

decodeCondBlocks — ⚪ definition

def · source

def decodeCondBlocks (cond : Option Json) : CondBlocks × List CondWarning

evalCond_noContext_tu — 🟢 proved

theorem · source

theorem evalCond_noContext_tu (blocks : CondBlocks) :
    (evalCond noContext blocks).1 = .t ∨ (evalCond noContext blocks).1 = .u

evalCond_noContext_T_imp — 🟢 proved

theorem · source

theorem evalCond_noContext_T_imp (blocks : CondBlocks) (ctx : CondContext)
    (h : (evalCond noContext blocks).1 = .t) :
    (evalCond ctx blocks).1 = .t