Redex implementation of L3