BDD on GearsAgda

Binary decision diagram on GearsAgda

Lightweight continuation form ( I → ( O → t) → t ), i.e. loop

maximum sharing with fixed term ordering