DynamicsDebug.mmt

namespace http://mathhub.info/FrameIT/frameworld/integrationtests/dynamicsdebug ❚

rule scala://parser.api.mmt.kwarc.info?MMTURILexer ❚

import frameworld http://mathhub.info/FrameIT/frameworld ❚
fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚

theory IfElseDebug =
    if_then_elsex: {A: 𝒰 100} bool ⟶ A ⟶ A ⟶ A ❘ # ifx 2 thenx 3 elsex 4 ❙
    simplify_ifelse1: {A: 𝒰 100, a: A, b: A} ⊦ (ifx true  thenx a elsex b) ≐ a ❘ role Simplify ❙
    simplify_ifelse2: {A: 𝒰 100, a: A, b: A} ⊦ (ifx false thenx a elsex b) ≐ b ❘ role Simplify ❙

    c = ifx true thenx 1.0 elsex 0.0 ❙
❚

// theory StepUntilDebug =
    include ☞http://mathhub.info/FrameIT/frameworld?StepUntil ❙
    my_list: List[ℝ] ❘ = stepUntil 0.0 ([x: ℝ] plus_real_lit x 1.0) ([x: ℝ] leq_real_lit 10.0 x) ❙
❚