tricu/demos/size.tri

compose = \f g x : f (g x)

succ = y (\self :
  triage
    1
    t
    (triage
      (t (t t))
      (\_ tail : t t (self tail))
      t))

size = (\x :
  (y (\self x :
    compose succ
      (triage
        (\x : x)
        self
        (\x y : compose (self x) (self y))
        x)) x 0))

size size
Allow lambda expressions without explicit paren 2025-01-26 08:52:28 -06:00			`compose = \f g x : f (g x)`
Add size demo 2025-01-23 18:57:59 -06:00
Definition dependency analysis tricu now allows defining terms in any order and will resolve dependencies to ensure that they're evaluated in the right order. Undefined terms are detected and throw errors during dependency ordering. For now we can't define top-level mutually recursive terms. 2025-01-26 14:50:15 -06:00			`succ = y (\self :`
			`triage`
			`1`
			`t`
			`(triage`
			`(t (t t))`
			`(\_ tail : t t (self tail))`
Add size demo 2025-01-23 18:57:59 -06:00			`t))`

Definition dependency analysis tricu now allows defining terms in any order and will resolve dependencies to ensure that they're evaluated in the right order. Undefined terms are detected and throw errors during dependency ordering. For now we can't define top-level mutually recursive terms. 2025-01-26 14:50:15 -06:00			`size = (\x :`
			`(y (\self x :`
			`compose succ`
			`(triage`
			`(\x : x)`
			`self`
			`(\x y : compose (self x) (self y))`
Add size demo 2025-01-23 18:57:59 -06:00			`x)) x 0))`
Eval optimization! Tests for demos 2025-01-25 09:18:13 -06:00
			`size size`