Agda.TypeChecking.Monad.Open
makeOpen
makeClosed
getOpen
tryOpen