Agda.TypeChecking.Monad.Open
makeOpen
makeClosed
isClosed
getOpen
tryOpen