Another positive train journey, this time with Tree Equality:

```
Positive.decEq (Node (the Nat 3) Leaf Leaf) (Node 3 Leaf (Node 4 Leaf Leaf))
Left (CmpNoRight CmpHeavyR)
```

```
Positive.decEq (Node 3 Leaf (Node 4 Leaf Leaf)) (Node 3 Leaf (Node (the Nat 4) Leaf Leaf))
Right (CmpT (Succ (Succ (Succ Zero))) CmpH (CmpT (Succ (Succ (Succ (Succ Zero)))) CmpH CmpH))
```

```
Positive.decEq (Node 3 Leaf (Node 4 Leaf Leaf)) (Node 3 Leaf (Node (the Nat 5) Leaf Leaf))
Left (CmpNoRight (CmpNoHead (MoreBoth (MoreBoth (MoreBoth (MoreBoth MoreRight))))))
```

#dependent_types #idris2 #constructive_negation

Look 'Ma' still no Void, ergonomics aside, *I* think this is cool. I am hoping #TYPES2025 will do too!

```
λΠ> Tree.ALL.all {p=GT 3} (\x => (GreaterThan.isGT 3 x)) (Node 6 Leaf (Node 7 Leaf Leaf))
Left (Here (LTESucc (LTESucc (LTESucc LTEZero))))
```

```
λΠ> decEq [Z,(S Z),(S (S Z))] [1,2,3]
Left (HeadNot MoreRight)
λΠ> decEq [Z,(S Z),(S (S Z))] [Z,(S Z),(S (S Z))]
Right (There Zero (There (Succ Zero) (There (Succ (Succ Zero)) Here)))
λΠ>
```

#dependent_types #constructive_negation #decidability #ITP