diff --git a/presentation/sections/03_midas.typ b/presentation/sections/03_midas.typ index 23bae00..259223d 100644 --- a/presentation/sections/03_midas.typ +++ b/presentation/sections/03_midas.typ @@ -404,8 +404,8 @@ Steps: row-gutter: 1em, [AST], none, none, text(size: 2em)[+], - text(size: 2em)[$stretch(->)^#{set text(size: 0.6em);```py ast.unparse(tree)```}$], - [Code], + uncover("2-", text(size: 2em)[$stretch(->)^#{set text(size: 0.6em);```py ast.unparse(tree)```}$]), + uncover("2-")[Code], [Typing\ Judgements], ) ) @@ -453,7 +453,6 @@ Steps: def __truediv__: fn(float, /) -> Meter } ``` - - Dependent Types (i.e. with value constraints) ```midas 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() ``` +#pause + #figure( align( left + top, @@ -565,12 +566,10 @@ $ overline(x) = 1 / n sum_(i=0)^n x_i $ -#alternatives[ - $ - "type_of"(overline(x)) = "type_of"( ("type_of"(x) + "type_of"(x)) / "int" ) - $ -][ - $ - "type_of"(overline(x)) = "type_of"( ("Meter" + "Meter") / "int") = "Meter" - $ -] \ No newline at end of file +#pause + +$ + "type_of"(overline(x)) &= "type_of"( ("type_of"(x) + "type_of"(x)) / "type_of"(n) )\ + pause + &= "type_of"( ("Meter" + "Meter") / "int") pause = "Meter" +$