Channels

#linking-together

Title

# linking-together

c

Chris G

05/23/2022, 11:20 PM"Yatima is a pure functional programming language implemented in Rust with... content addressing, first-class types, linear, affine and erased types, type-safe dependent metaprogramming"

Copy code

```
type Vector (A: Type): ∀ (ω k: Natural) -> Type {
Nil: Vector A Natural.Z,
Cons (0 k: Natural) (x: A) (xs: Vector A k): Vector A (Natural.S k),
}
def Vector.head (0 A: Type) (k: Natural) (a : Vector A (Natural.S k)): A
= ((case a) (λ k' self => ∀ (Equal Natural (Natural.S k) k') -> A)
(λ e => Empty.absurd A (Natural.Z_isnt_S k e))
(λ k x xs e => x))
(Equal.Refl Natural (Natural.S k))
```

https://github.com/yatima-inc/yatima-lang-alpha👀 2

3 Views