module Agda.TypeChecking.ProjectionLike where import Agda.Syntax.Abstract.Name (QName) import Agda.TypeChecking.Monad.Base makeProjection :: QName -> TCM () eligibleForProjectionLike :: QName -> TCM Bool