def DY.Traceful [ExecTraceTypes] (a : Type) : Type

Equations

• DY.Traceful a = ((trIn : DY.ExecTrace) → Option a × { trOut : DY.ExecTrace // trIn ≤ trOut })

@[instance_reducible]

instance DY.instMonadTraceful [ExecTraceTypes] : Monad Traceful

Equations

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

@[instance_reducible]

instance DY.instAlternativeTraceful [ExecTraceTypes] : Alternative Traceful

Equations

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

def DY.Traceful.run {a : Type} [ExecTraceTypes] (x : Traceful a) (tr : ExecTrace) : Option a × { trOut : ExecTrace // tr ≤ trOut }

Equations

• x.run tr = x tr

def DY.Traceful.mk [ExecTraceTypes] {α : Type} (f : (tr : ExecTrace) → Option α × { trOut : ExecTrace // tr ≤ trOut }) : Traceful α

Equations

• DY.Traceful.mk f = f

@[implicit_reducible]

def DY.Err (α : Type u_1) : Type u_1

Equations

• DY.Err = OptionT Id

@[instance_reducible]

instance DY.instMonadErr : Monad Err

Equations

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

@[instance_reducible]

instance DY.instAlternativeErr : Alternative Err

Equations

• DY.instAlternativeErr = { toApplicative := DY.instMonadErr.toApplicative, failure := @DY.instAlternativeErr._aux_1, orElse := @DY.instAlternativeErr._aux_3 }

@[instance_reducible]

instance DY.instMonadLiftErrTraceful [ExecTraceTypes] : MonadLift Err Traceful

Equations

• DY.instMonadLiftErrTraceful = { monadLift := fun {α : Type} (x : DY.Err α) => DY.Traceful.mk fun (tr : DY.ExecTrace) => (x, ⟨tr, ⋯⟩) }

theorem DY.Traceful.run_mk [ExecTraceTypes] {α : Type} (f : (tr : ExecTrace) → Option α × { trOut : ExecTrace // tr ≤ trOut }) : (mk f).run = f

theorem DY.Traceful.run_pure {a : Type} [ExecTraceTypes] (x : a) (tr : ExecTrace) : (pure x).run tr = (some x, ⟨tr, ⋯⟩)

theorem DY.Traceful.run_bind {a b : Type} [ExecTraceTypes] (x : Traceful a) (f : a → Traceful b) (tr : ExecTrace) : (x >>= f).run tr = match x.run tr with | (opt_x, tr_1) => match opt_x with | some x => match (f x).run tr_1.val with | (opt_y, tr_2) => (opt_y, ⟨tr_2.val, ⋯⟩) | none => (none, tr_1)

theorem DY.Traceful.run_failure {a : Type} [ExecTraceTypes] (tr : ExecTrace) : failure.run tr = (none, ⟨tr, ⋯⟩)