From 7e5ea5e41432e719ab7b9ef8d408a8a91036d5e2 Mon Sep 17 00:00:00 2001 From: LordBaryhobal Date: Mon, 22 Jun 2026 15:29:39 +0200 Subject: [PATCH] chore: add example to demonstrate some features --- examples/02_demonstration/demo.midas | 10 ++++++++++ examples/02_demonstration/demo.py | 19 +++++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 examples/02_demonstration/demo.midas create mode 100644 examples/02_demonstration/demo.py diff --git a/examples/02_demonstration/demo.midas b/examples/02_demonstration/demo.midas new file mode 100644 index 0000000..394cc15 --- /dev/null +++ b/examples/02_demonstration/demo.midas @@ -0,0 +1,10 @@ +predicate in_range(min: float, max: float)(v: float) = min <= v & v <= max +predicate is_ratio = in_range(0, 1) + +type Money = float +type Price[T <: Money] = T where _ >= 0 + +type EUR = Money +type USD = Money + +type Reduction = float where is_ratio(_) diff --git a/examples/02_demonstration/demo.py b/examples/02_demonstration/demo.py new file mode 100644 index 0000000..20e5bb5 --- /dev/null +++ b/examples/02_demonstration/demo.py @@ -0,0 +1,19 @@ +from typing import TypeVar, cast + +from demo_stubs import EUR, USD, Money, Price, Reduction + +T = TypeVar("T", bound=Money) + + +def apply_reduction(amount: Price[T], reduction: Reduction) -> Price[T]: + return cast(Price[T], (1.0 - reduction) * amount) + + +a1 = cast(Price[EUR], 3.2) +a2 = cast(Price[USD], 10.4) +r1: Reduction = cast(Reduction, 0.2) + +print(apply_reduction(a1, r1)) +print(apply_reduction(a2, r1)) + +# a3 = a1 + a2