module extra where

-- intrinsically typed closure calculus
import extra.clos

-- intrinsically typed explicit substitution
import extra.es  -- basic rewriting system
import extra.esn -- (full) normal order reudction

-- intrinsically typed stlc with recursive type
-- adapted from *System F in Agda, for Fun and Profit*
import extra.mu

-- TODO wsdb system f
-- import extra.sf