nix flake update Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
use janestreet format style Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
nix flake update Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
nix flake update Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
correct the dependencies Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
prepare for sublibraries separation Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
extract Unification module Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
lambda unify with arbitrary value t We can consider some examples, e.g. suc ?= \x -> suc x they should be considered the same, then if we create a rigid n, now we are asking about suc n ?= (\x -> suc x) n = suc n Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
improve error message Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
file suffix Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
replace shadow traceln with Reporter tracef Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
replace Eio.traceln with Reporter tracef This is a better solution, since only when error occurs, we will get these messages. Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
placeholder for pi Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
typo Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
also add implicit pi type parser Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
provide infix combinator & shorten the example Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
most parser of inductive types Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
draft of inductive data type Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
format Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>
author name changed Signed-off-by: Lîm Tsú-thuàn <inbox@dannypsnl.me>