ProjectionLike.hs-boot

module Agda.TypeChecking.ProjectionLike where

import Agda.Syntax.Abstract.Name (QName)
import Agda.TypeChecking.Monad.Base

makeProjection :: QName -> TCM ()
eligibleForProjectionLike :: QName -> TCM Bool