dynamics.mmt

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

import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚
import rules scala://rules.frameit.mmt.kwarc.info ❚
fixmeta ?FrameworldMeta ❚
theory StepUntil =
    // {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❙
    stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❘ # stepUntil 1 2 3 4 ❙
    //stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ X ❘ # stepUntil 1 2 3 4 ❙
    rule rules?StepUntilRule (true) ❙
❚
theory StepUntilX =
    stepUntilX : {A: type}{B: type}{C: type} B ⟶ C ⟶ A ⟶ (B ⟶ C ⟶ A ⟶ A) ⟶ (A ⟶ bool) ⟶ List[A] ❘ # stepUntilX 1 2 3 4 5 6 7 8 ❙
    rule rules?StepUntilXRule (true) ❙
❚
theory IfThenElseX =
    // {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❙
    ifthenelsex : {X: type} bool ⟶ X ⟶ X ⟶ X ❘ # 1 ifx 2 thenx 3 elsex 4 ❙
    rule rules?IfThenElseRuleX (true) (false) ❙
❚