examples

examples/b2t2/access-subcomponents/getColumn2.tt

@@ -0,0 +1,3 @@
+def getColumn :
+  ∀ r : R *, l : L, t : *. ⟨l ▹ t⟩ ≲(C) r ⇒ List (Π(C) r) → ⌊l⌋ → List t =
+  \tb l. map (\r. (prj r)/l) tb

examples/b2t2/access-subcomponents/getRow.tt

@@ -0,0 +1 @@
+def getRow : ∀ r : R *, u : U. List (Π(u) r) → Int → Option (Π(u) r) = get

examples/b2t2/access-subcomponents/getValue.tt

@@ -0,0 +1,3 @@
+def getValue : ∀ r : R *, l : L, t : *.
+    ⟨l ▹ t⟩ ≲(C) r ⇒ List (Π(C) r) → Int → ⌊l⌋ → Option t =
+  \tb n l. omap (\r. (prj r)/l) (get tb n)

examples/b2t2/aggregate/bin.tt

@@ -0,0 +1,19 @@
+def bin : ∀ r : R *, l : L. ⟨l ▹ Int⟩ ≲(C) r ⇒ List (Π(C) r) → ⌊l⌋ → Int →
+    List (Π(N) ⟨'lower' ▹ Int, 'upper' ▹ Int, 'count' ▹ Int⟩) =
+  \tb l n.
+    if n == 0 then
+      nil
+    else
+      let values = map (\r. (prj r)/l) tb in
+      let count = \lower upper. lcount (\v. and (lower <= v) (v < upper)) values
+      in
+      let lower = min values in
+      let upper = max values + 1 in
+      let diff = max - min in
+      let preBins = map
+        (\i. {'lower' ▹ min + diff * i, 'upper' ▹ min + diff * (i + 1)})
+        (range (n - 1))
+      in
+      let bins = snoc preBins {'lower' ▹ min + diff * (n - 1), 'upper' ▹ upper}
+      in
+      map (\b. b ++ {'count' ▹ count (prj b)/'lower' (prj b)/'upper'}) bins

examples/b2t2/aggregate/count.tt

@@ -0,0 +1,5 @@
+def count : ∀ r : R *, l : L, t : *. Eq t, ⟨l ▹ t⟩ ≲(C) r ⇒
+    List (Π(C) r) → ⌊l⌋ → List (Π(N) ⟨'value' ▹ t, 'count' ▹ Int⟩) =
+  \tb l.
+    let ks = unique (map (\r. (prj r)/l) tb) in
+    map (\k. lcount (\r. eq k (prj r)/l) tb) ks

examples/b2t2/aggregate/groupBy.tt

@@ -0,0 +1,5 @@
+def groupBy : ∀ r r' : R *, tk tv : *, u u' : U. Eq tk ⇒ List (Π(u) r) →
+    (Π(u) r → tk) → (Π(u) r → tv) → (tk → tv → Π(u') r') → List (Π(u') r') =
+  \tb kf pf af.
+    let ks = unique (map kf tb) in
+    map (\k. af k (map pf (filter (\r. kf r == k) tb))) ks

examples/b2t2/aggregate/pivotTable.tt

@@ -0,0 +1,9 @@
+def pivotTable : ∀ r rg r' : R *, li lo : L, ti to : *, u : U.
+    All Eq rg, rg ≲(C) r, ⟨li ▹ ti⟩ ≲(C) r, rg ⊙(u) ⟨lo ▹ to⟩ ~ r' ⇒
+    List (Π(C) r) → Labels u rg → ⌊li⌋ → ⌊lo⌋ → (List ti → to) →
+	List (Π(u) r') =
+  \tb _ li lo f.
+    let groups = unique (map (\r. prj r : Π(C) rg) tb) in
+    map (\g. orderₚ rg g ++
+          {lo ▹ f (map (\r. (prj r)/li) 5)})
+      groups

examples/b2t2/constructors/addColumn.tt

@@ -0,0 +1,3 @@
+def addColumn : ∀ r r' : R *, l : L, t : *. r ⊙(N) ⟨l ▹ t⟩ ~ r' ⇒
+    List (Π(N) r) → ⌊l⌋ → List t → List (Π(N) r') =
+  \tb l col. zip (\o e. o ++ {l ▹ e}) tb col

examples/b2t2/constructors/addRows.tt

@@ -0,0 +1,2 @@
+def addRows : ∀ r : R *, u : U. List (Π(u) r) → List (Π(u) r) → List (Π(u) r) =
+  append

examples/b2t2/constructors/buildColumn.tt

@@ -0,0 +1,3 @@
+def buildColumn : ∀ r r' : R *, l : L, t : *. r ⊙(N) ⟨l ▹ t⟩ ~ r' ⇒
+    List (Π(N) r) → ⌊l⌋ → (Π(N) r → t) → List (Π(N) r') =
+  \tb l f. map (\o. o ++ {l ▹ f o}) tb

examples/b2t2/constructors/crossJoin.tt

@@ -0,0 +1,3 @@
+def crossJoin : ∀ rl rr r : R *. rl ⊙(N) rr ~ r ⇒
+    List (Π(N) rl) → List (Π(N) rr) → List (Π(N) r) =
+  \tbl tbr. map (\l. map (\r. l ++ r) tbr) tbl

examples/b2t2/constructors/emptyTable.tt

@@ -0,0 +1 @@
+def emptyTable : List Unit = nil

examples/b2t2/constructors/hcat.tt

@@ -0,0 +1,2 @@
+def hcat : ∀ rl rr r : R *. rl ⊙(N) rr ~ r ⇒
+    List (Π(N) rl) → List (Π(N) rr) → List (Π(N) r) = zip (\l r. l ++ r)

examples/b2t2/constructors/leftJoin.tt

@@ -0,0 +1,13 @@
+def leftJoin : ∀ rc rl' rr' rl rr r : R *, u : U.
+    All Eq rc, rc ⊙(u) rl' ~ rl, rc ⊙(u) rr' ~ rr, rl ⊙(u) Lift Option rr' ~ r ⇒
+    List (Π(u) rl) → List (Π(u) rr) → LabelSet rc → List (Π(u) r) =
+  \tbl tbr _. map (\r.
+    let eqr = filter (\r'. eq (prj r : Π(u) rc) (prj r' : Π(u) rc)) tbr in
+    if length eqr > 0 then
+      map (\r'. r ++ prj r') eqr
+    else
+      let nones = ind (\a : R *. Π(C) (Lift Option a)) rr' (\l acc.
+        acc ++ {l ▹ none}
+      ) {} in
+      singleton (r ++ nones)
+  ) tbl

examples/b2t2/constructors/values.tt

@@ -0,0 +1 @@
+def values : ∀ r : R *, u : U. List (Π(u) r) → List (Π(u) r) = \tb. tb

examples/b2t2/constructors/vcat.tt

@@ -0,0 +1,2 @@
+def vcat : ∀ r : R *, u : U. List (Π(u) r) → List (Π(u) r) → List (Π(u) r) =
+  append

examples/b2t2/data-cleaning/pivotLonger.tt

@@ -0,0 +1,7 @@
+def pivotLonger : ∀ r rk rr r' : R *, lk lv : L, t : *.
+    rr ⊙(C) Lift (Const t) rk ~ r,
+    rr ⊙(C) ⟨lk ▹ Σ(C) (Lift (Const Unit) rk), lv ▹ t⟩ ~ r' ⇒
+    List (Π(C) r) → LabelSet rk → ⌊lk⌋ → ⌊lv⌋ → List (Π(C) r') =
+  \tb _ lk lv. lflatten (map (\r. map (\kv. (prj r : Π(C) rr) ++ kv)
+    (ind (\_ : *. List (Π(N) ⟨lk ▹ Σ(C) (Lift (Const Unit) rk), lv ▹ t⟩)) rk
+      (\l acc. {lk ▹ inj [l ▹ {}], lv ▹ (prj r)/l} :: acc) nil)) tb)

examples/b2t2/data-cleaning/pivotWider.tt

@@ -0,0 +1,29 @@
+def pivotWider : ∀ r rk rr r' : R *, lk lv : L, t : *, u : U. All Eq rr,
+    rr ⊙(u) ⟨lk ▹ Σ(u) (Lift (Const Unit) rk), lv ▹ t⟩ ~ r,
+    rr ⊙(u) Lift (Const (Option t)) rk ~ r' ⇒
+    List (Π(u) r) → ⌊lk⌋ → ⌊lv⌋ → List (Π(u) r') =
+  \tb lk lv.
+    let groups = fold (\r acc.
+      let res = fold (\group acc.
+        if and (not acc/'found') (rowEq group/'shared' (prj r)) then
+          {
+            'updated' ▹ {
+              'shared' ▹ group/'shared',
+              'kvs' ▹ prj r ++ group/'kvs'
+            } :: acc/'updated',
+            'found' ▹ true
+          }
+        else
+          {'updated' ▹ group :: acc/'updated', 'found' ▹ acc/'found'}
+      ) {'updated' ▹ nil, 'found' ▹ false} acc in
+      if res/'found' then
+        res/'updated'
+      else
+        {'shared' ▹ prj r, 'shared' ▹ singleton (prj r)} :: acc
+    ) tb in
+    map (\group.
+      group/'shared' ++ ind (\a : R *. Π(u) (Lift (Const (Option t)) a)) rk
+        (\l acc. acc ++ {l ▹ fold (\kv acc.
+          if and (isNone acc) (is l kv/lk) then some kv/lv else acc
+        ) none group/'kvs'}) {}
+    ) groups

examples/b2t2/missing-values/completeCases.tt

@@ -0,0 +1,3 @@
+def completeCases : ∀ r : R *, l : L, t : *. ⟨l ▹ Option t⟩ ≲(C) r ⇒
+    List (Π(C) r) → ⌊l⌋ → List Bool =
+  \tb l. map (\r. isSome (prj r)/l) tb

examples/b2t2/missing-values/dropna.tt

@@ -0,0 +1,10 @@
+def dropna : ∀ r rm rr r' : R *. Split Option rm rr r, rm ⊙(C) rr ~ r' ⇒
+    List (Π(C) r) → List (Π(C) r') =
+  filterMap (\r.
+    let s = splitₚ Option r in
+    let m = (prj s)/'match' in
+    omap (\unwrapped. unwrapped ++ (prj s)/'rest')
+      (ind (\a : R *. Option (Π(C) a)) rm (\l.
+        bind (\acc. map (\x. acc ++ {l ▹ x}) (prj m)/l)
+      ) (some {}))
+  )

examples/b2t2/missing-values/fillna.tt

@@ -0,0 +1,4 @@
+def fillna : ∀ r ro r' : R *, l : L, t : *.
+    ⟨l ▹ Option t⟩ ⊙(C) ro ~ r, ⟨l ▹ t⟩ ⊙(C) ro ~ r' ⇒
+    List (Π(C) r) → ⌊l⌋ → t → List (Π(C) r') =
+  \tb l default. map (\r. prj r ++ {l ▹ ogetD (prj r)/l default}) tb

examples/b2t2/ordering/orderBy.tt

@@ -0,0 +1,25 @@
+type Compare =
+  \r : R *, u : U, a : *. Π(N) ⟨'getKey' ▹ Π(u) r → a, 'compare' ▹ a → a → Bool⟩
+
+def orderBy : ∀ r rk : R *, u : U.
+    List (Π(u) r) → Π(N) (Lift (Compare r u)) rk → List (Π(u) r) =
+  \tb cs.
+    let rowsAndKeys = map (\r. {
+      'row' ▹ r,
+      'keys' ▹ ind Π(N) rk (\l acc. acc ++ {l ▹ (prj (prj cs)/l)/'getKey' r}) {}
+    }) tb in
+    let cs' = ind (\a : R *. Π(N) (Lift (\a : *. a → a → Bool) a)) rk
+      (\l acc. acc ++ {l ▹ (prj (prj cs)/l)/'compare'}) {} in
+    let rowLe : Π(N) rk → Π(N) rk → Bool =
+      \r0 r1. ogetD (ind (Const (Option Bool)) rk (\l acc.
+        if isSome acc then
+          acc
+        else if and ((prj cs')/l (prj r0)/l (prj r1)/l)
+                  (le (prj r1)/l (prj r0)/l) then
+          none
+        else
+          some (le (prj r0)/l (prj r1)/l)
+      ) none) true
+    in
+    map (\rk. (prj rk)/'row')
+      (sortBy (\r0 r1. rowLe (prj r0) (prj r1)) tb)

examples/b2t2/ordering/sortByColumns.tt

@@ -0,0 +1,14 @@
+def sortByColumns : ∀ r r' : R *, u : U. r' ≲(u) r, All LE r' ⇒
+    List (Π(u) r) → LabelList r' → List (Π(u) r) =
+  \tb _.
+    let rowLe : Π(N) r' → Π(N) r' → Bool =
+      \r0 r1. ogetD (ind (Const (Option Bool)) r' (\l acc.
+        if isSome acc then
+          acc
+        else if and (le (prj r0)/l (prj r1)/l) (le (prj r1)/l (prj r0)/l) then
+          none
+        else
+          some (le (prj r0)/l (prj r1)/l)
+      ) none) true
+    in
+    sortBy (\r0 r1. rowLe (prj r0) (prj r1)) tb

examples/b2t2/ordering/tsort.tt

@@ -0,0 +1,7 @@
+def tsort : ∀ r : R *, l : L, t : *, u : U.
+    ⟨l ▹ t⟩ ≲(C) r, LE t ⇒ List (Π(u) r) → ⌊l⌋ → Bool → List (Π(u) r) =
+  \tb l asc.
+    if asc then
+      sortBy (\r0 r1. le (prj (r0 : Π(C) r))/l (prj (r1 : Π(C) r))/l) tb
+    else
+      sortBy (\r0 r1. le (prj (r1 : Π(C) r))/l (prj (r0 : Π(C) r))/l) tb

examples/b2t2/properties/header.tt

@@ -0,0 +1,2 @@
+def header : ∀ r : R *, u : U. List (Π(u) r) → Labels u r =
+  \_. ind (Labels u) r (\l acc. acc ++ {l ▹ {}}) {}

examples/b2t2/properties/ncols.tt

@@ -0,0 +1,2 @@
+def ncols : ∀ r : R *. List (Π(C) r) → Int =
+  ind (Const Int) r (\_ acc. acc + 1) 0

examples/b2t2/properties/nrows.tt

@@ -0,0 +1 @@
+def nrows : ∀ r : R *, u : U. List (Π(u) r) → Int = length

examples/b2t2/subtable/distinct.tt

@@ -0,0 +1,2 @@
+def distinct : ∀ r : R *, u : U. All Eq r ⇒ List (Π(u) r) → List (Π(u) r) =
+  unique

examples/b2t2/subtable/dropColumn.tt

@@ -0,0 +1,2 @@
+def dropColumn : ∀ r r' : R *, l : L, t : *. r' ⊙(C) ⟨l ▹ t⟩ ~ r ⇒
+    List (Π(C) r) → ⌊l⌋ → List (Π(C) r') = \tb _. map (\r. prj r) tb

examples/b2t2/subtable/dropColumns.tt

@@ -0,0 +1,3 @@
+def dropColumns : ∀ r rd r' : R *, u : U. r' ⊙(C) rd ~ r ⇒
+    List (Π(u) r) → LabelSet rd → List (Π(u) r') =
+  \tb _. map (\r. orderₚ r' (prj (r : Π(C) r))) tb

examples/b2t2/subtable/head.tt

@@ -0,0 +1,5 @@
+def head : ∀ r : R *, u : U. List (Π(u) r) → Int → List (Π(u) r) =
+  \tb i. if i >= 0 then
+    take (0 - i) tb
+  else
+    drop (length tb + i) tb

examples/b2t2/subtable/selectColumns3.tt

@@ -0,0 +1,3 @@
+def selectColumns : ∀ r r' : R *, u : U. r' ≲(C) r ⇒
+    List (Π(C) r) → LabelList r' → List (Π(N) r') =
+  \tb _. map (\r. orderₚ r' (prj r)) tb

examples/b2t2/subtable/selectRows1.tt

@@ -0,0 +1,2 @@
+def selectRows1 : ∀ r : R *, l : L, t : *, u : U.
+    List (Π(u) r) → List Int → List (Π(u) r) = \tb. map (get tb)

examples/b2t2/subtable/selectRows2.tt

@@ -0,0 +1,3 @@
+def selectRows2 :
+  ∀ r : R *, l : L, t : *, u : U. List (Π(u) r) → List Bool → List (Π(u) r) =
+  \tb bs. filter (\x. x) (zip (\r b. if b then some r else none) tb bs)

examples/b2t2/subtable/tfilter.tt

@@ -0,0 +1,2 @@
+def tfilter : ∀ r : R *, u : U.
+  List (Π(u) r) → (Π(u) r → Bool) → List (Π(u) r) = flip filter

examples/b2t2/utilities/find.tt

@@ -0,0 +1,2 @@
+def find : ∀ r : R *. All Eq r ⇒ List (Π(C) r) → Π(C) r → Option Int =
+  \tb r. foldIdx (\r' i. orElse (if rowEq r r' then some i else none)) none tb

examples/b2t2/utilities/flatten.tt

@@ -0,0 +1,14 @@
+def flatten :
+  ∀ r rs rr r' : R *. Lift (\a : *. List a) rs ⊙(C) rr ~ r, rs ⊙(C) rr ~ r' ⇒
+    List (Π(C) r) → LabelSet rs → List (Π(C) r') =
+  \tb _. lflatten (map (\r.
+    let s : Π(C) (Lift List rs) = prj r in
+    let rr : Π(C) rr = prj r in
+    let s' = ind (\a : R *. Σ(N) ⟨'many' ▹ List (Π(C) rs), 'one' ▹ Π(C) rs⟩) rs
+      (\l.
+        (\x. ['many' ▹ map (\y. x/'one' ++ {l ▹ y}) s/l]) ▿
+          (\xs. ['many' ▹ zip (\v r'. r' ++ {l ▹ v}) s/l xs/'many'])
+      ) ['one' ▹ {}]
+    in
+    (\x. singleton x/'one') ▿ (\x. x/'many') s' ++ rr
+  ) tb)

examples/b2t2/utilities/groupByRetentive.tt

@@ -0,0 +1,5 @@
+def groupByRetentive : ∀ r : R *, l : L, t : *, u : U. Eq t, ⟨l ▹ t⟩ ≲(C) r ⇒
+    List (Π(u) r) → ⌊l⌋ → ⟨'key' ▹ t, 'groups' ▹ List (Π(u) r)⟩ =
+  \tb l.
+    let keys = unique (map (\r. (prj r)/l) tb) in
+	map (\k. {'key' ▹ k, 'groups' ▹ filter (\r. eq (prj r)/l k) tb}) keys

examples/b2t2/utilities/groupBySubtractive.tt

@@ -0,0 +1,7 @@
+def groupBySubtractive : ∀ r r' : R *, l : L, t : *. Eq t, r' ⊙(C) ⟨l ▹ t⟩ ~ r ⇒
+    List (Π(C) r) → ⌊l⌋ → ⟨'key' ▹ t, 'groups' ▹ List (Π(C) r')⟩ =
+  \tb l.
+    let keys = unique (map (\r. (prj r)/l) tb) in
+	map (\k.
+	  {'key' ▹ k, 'groups' ▹ map (\r. prj r) (filter (\r. eq (prj r)/l k) tb)}
+	) keys

examples/b2t2/utilities/groupJoin.tt

@@ -0,0 +1,8 @@
+def groupJoin : ∀ r0 r1 r : R *, t : *, u0 u1 u : U. Eq t ⇒
+    List (Π(u0) r0) → List (Π(u1) r1) → (Π(u0) r0 → t) → (Π(u1) r1 → t) →
+    (Π(u0) r0 → List (Π(u1) r1) → Π(u) r) → List (Π(u) r) =
+  \tb0 tb1 k0f k1f af.
+    map (\r0.
+      let k0 : t = k0f r0 in
+      af r0 (filter (\r1. eq k0 (k1f r1)) tb1)
+    ) tb0

examples/b2t2/utilities/join.tt

@@ -0,0 +1,8 @@
+def join : ∀ r0 r1 r : R *, t : *, u0 u1 u : U. Eq t ⇒
+    List (Π(u0) r0) → List (Π(u1) r1) → (Π(u0) r0 → t) → (Π(u1) r1 → t) →
+    (Π(u0) r0 → Π(u1) r1 → Π(u) r) → List (Π(u) r) =
+  \tb0 tb1 k0f k1f cf.
+    map (\r0.
+      let k0 : t = k0f r0 in
+      filterMap (\r1. if eq k0 (k1f r1) then some (cf r0 r1) else none) tb1
+    ) tb0

examples/b2t2/utilities/renameColumn.tt

@@ -0,0 +1,4 @@
+def renameColumn :
+  ∀ r rr r' : R *, l l' : L, t : *. rr ⊙(C) ⟨l ▹ t⟩ ~ r, rr ⊙(C) ⟨l' ▹ t⟩ ~ r' ⇒
+    List (Π(C) r) → ⌊l⌋ → ⌊l'⌋ → List (Π(C) r') =
+  \tb l l'. map (\r. prj r ++ {l' ▹ (prj r)/l}) tb

examples/b2t2/utilities/select.tt

@@ -0,0 +1,2 @@
+def select : ∀ r r' : R *, u u' : U.
+    List (Π(u) r) → (Π(u) r → Int → Π(u') r') → List (Π(u') r') = flip mapIdx

examples/b2t2/utilities/selectMany.tt

@@ -0,0 +1,8 @@
+def selectMany : ∀ r r' r'' : R *, u u' u'' : U. List (Π(u) r) →
+    (Π(u) r → Int → List (Π(u') r')) → (Π(u) r → Π(u') r' → Π(u'') r'') →
+    List (Π(u'') r'') =
+  \tb pf rf.
+    let pairs : List (Π(N) ⟨'orig' ▹ Π(u) r, 'prj' ▹ Π(u') r'⟩) =
+      flatten (mapIdx (\r idx. map (\p. {'orig' ▹ r, 'prj' ▹ p}) (pf r idx)) tb)
+    in
+    map (\op. rf (prj op)/'orig' (prj op)/'prj') pairs

examples/b2t2/utilities/transformColumn.tt

@@ -0,0 +1,4 @@
+def transformColumn :
+  ∀ r rr r' : R *, l : L, t t' : *. rr ⊙(C) ⟨l ▹ t⟩ ~ r, rr ⊙(C) ⟨l ▹ t'⟩ ~ r' ⇒
+    List (Π(C) r) → ⌊l⌋ → (t → t') → List (Π(C) r') =
+  \tb l f. map (\r. prj r ++ {l ▹ f (prj r)/l}) tb

examples/b2t2/utilities/update.tt

@@ -0,0 +1,4 @@
+def update : ∀ r rs rd rn r' : R *, u : U.
+    rs ⊙(C) rd ~ r, rs ⊙(C) rn ~ r', LabelsMatch rs rn ⇒
+    List (Π(u) r) → (Π(u) r → Π(C) rn) → List (Π(C) r') =
+  \tb f. map (\r. (prj r : Π(C) rs) ++ (f r)) tb

examples/core/And.tt

@@ -0,0 +1 @@
+type And = \r : R C. All (\c : C. c) r

examples/core/Bool.tt

@@ -0,0 +1,14 @@
+type Bool = Σ(N) ⟨'false' ▹ Unit, 'true' ▹ Unit⟩
+
+def false : Bool = inj ['false' ▹ {}]
+
+def true : Bool = inj ['true' ▹ {}]
+
+def not : Bool → Bool =
+  ((\_. true) : Σ(N) ⟨'false' ▹ Unit⟩ → Bool) ▿ (\_. false)
+
+def and : Bool → Bool → Bool =
+  \x. ((\_. false) : Σ(N) ⟨'false' ▹ Unit⟩ → Bool) ▿ (\_. x)
+
+def or : Bool → Bool → Bool =
+  \x. ((\_. x) : Σ(N) ⟨'false' ▹ Unit⟩ → Bool) ▿ (\_. false)

examples/core/Const.tt

@@ -0,0 +1 @@
+type Const = \a b : *. b

examples/core/Eq.tt

@@ -0,0 +1,8 @@
+class Eq a : * where
+  eq : a → a → Bool
+
+instance Eq Int where
+  eq = \x y. x == y
+
+def rowEq : ∀ r : R *. All Eq r ⇒ Π(C) r → Π(C) r → Bool =
+  \x y. ind (\_ : R *. Bool) r (\l acc. and acc (eq (prj x)/l (prj y)/l)) true

examples/core/LE.tt

@@ -0,0 +1,5 @@
+class LE a : * where
+  le : a → a → Bool
+
+instance LE Int where
+  le = \x y. x <= y

examples/core/Labels.tt

@@ -0,0 +1,5 @@
+type Labels = \u : U, r : R *. Σ(u) (Lift (Const Unit) r)
+
+type LabelSet = Labels C
+
+type LabelList = Labels N

examples/core/LabelsMatch.tt

@@ -0,0 +1,4 @@
+def LabelsMatch = \r0 r1 : R *. And ⟨
+    Lift (\_ : *. ⟨ : * ⟩) r0 ≲(C) Lift (\_ : *. ⟨ : * ⟩) r1,
+    Lift (\_ : *. ⟨ : * ⟩) r1 ≲(C) Lift (\_ : *. ⟨ : * ⟩) r0
+  ⟩