HEL/TB-Docs
1
0
Fork 0
Code Issues Pull Requests Releases Activity

fix(presentation): tweak midas slides

Browse Source
This commit is contained in:
HEL
2026-08-21 17:16:48 +02:00
parent d1bece9cfe
commit d68352ba9b
1 changed files with 11 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files
presentation/sections/03_midas.typ
+11 -12
View File
@@ -404,8 +404,8 @@ Steps:
row-gutter: 1em, row-gutter: 1em,
[AST], none, none, [AST], none, none,
text(size: 2em)[+], text(size: 2em)[+],
text(size: 2em)[$stretch(->)^#{set text(size: 0.6em);```py ast.unparse(tree)```}$], uncover("2-", text(size: 2em)[$stretch(->)^#{set text(size: 0.6em);```py ast.unparse(tree)```}$]),
[Code], uncover("2-")[Code],
[Typing\ Judgements], [Typing\ Judgements],
) )
) )
@@ -453,7 +453,6 @@ Steps:
def __truediv__: fn(float, /) -> Meter def __truediv__: fn(float, /) -> Meter
} }
``` ```
- Dependent Types (i.e. with value constraints) - Dependent Types (i.e. with value constraints)
```midas ```midas
predicate in_range(mn: float, mx: float)(v: float) = mn <= v & v <= mx predicate in_range(mn: float, mx: float)(v: float) = mn <= v & v <= mx
@@ -533,6 +532,8 @@ Generates runtime checks
mean_height = df["height"].mean() mean_height = df["height"].mean()
``` ```
#pause
#figure( #figure(
align( align(
left + top, left + top,
@@ -565,12 +566,10 @@ $
overline(x) = 1 / n sum_(i=0)^n x_i overline(x) = 1 / n sum_(i=0)^n x_i
$ $
#alternatives[ #pause
$
"type_of"(overline(x)) = "type_of"( ("type_of"(x) + "type_of"(x)) / "int" ) $
$ "type_of"(overline(x)) &= "type_of"( ("type_of"(x) + "type_of"(x)) / "type_of"(n) )\
][ pause
$ &= "type_of"( ("Meter" + "Meter") / "int") pause = "Meter"
"type_of"(overline(x)) = "type_of"( ("Meter" + "Meter") / "int") = "Meter" $
$
]