This repository was archived by the owner on Jul 28, 2023. It is now read-only.
This repository was archived by the owner on Jul 28, 2023. It is now read-only.
Conversion checking modulo associativity #228
Description
Implementation note
eval : Term → VTerm
eval ((a + b) + c) = +[a, b, c]
eval (a + (b + c)) = +[a, b, c]
quote : VTerm → Term
quote +[a, b, c] = a + (b + c)