~dannypsnl/headvariant

Failed experiment: Refining inductive types with constructors subscripting
219449f3 — Lîm Tsú-thuàn 1 year, 4 months ago
add LICENSE
3340e05b — Lîm Tsú-thuàn 1 year, 5 months ago
fix, using bwd 2.2.0
4cb3e139 — Lîm Tsú-thuàn 1 year, 5 months ago
using `bwd`

refs

main
browse  log 

clone

read-only
https://git.sr.ht/~dannypsnl/headvariant
read/write
git@git.sr.ht:~dannypsnl/headvariant

You can also use your local clone with git send-email.

#head variant

Warning This is an early and experiemental project, it might likely contain bugs

This is an algebraic data type experiment, the project refines type with variant head, for example:

data Int where
  zero : Int[zero]
  pos : Int[pos, zero] -> Int[pos]
  neg : Int[neg, zero] -> Int[neg]
Do not follow this link