Home
last modified time | relevance | path

Searched refs:getCohesion (Results 1 – 15 of 15) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A DIrrelevance.hs188 case getCohesion thing of
201 let c = getCohesion a
250 $ applyCohesionToContext (getCohesion m)
409 mapCohesion (composeCohesion $ getCohesion a) mod
H A DMetaVars.hs1226 | getCohesion a1 /= getCohesion b1 -> patternViolation neverUnblock
1502 , modCohesion = max (getCohesion info) (getCohesion info')
H A DErrors.hs516 pwords "Cannot pattern match against" ++ [text $ verbalize $ getCohesion t] ++
695 verbalize $ getCohesion i]
H A DConversion.hs697 | not $ compareCohesion cmp (getCohesion dom1) (getCohesion dom2) -> errC
H A DCoverage.hs1158 let updCoh = composeCohesion (getCohesion info)
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DRecord.hs581 , "coh =" <+> (text . show) (getCohesion ai)
590 if hasLeftAdjoint (UnderComposition (getCohesion ai))
591 then unless (getCohesion ai == Continuous)
594 else genericError $ "Cannot have record fields with modality " ++ show (getCohesion ai)
H A DTerm.hs320 let (c :| cs) = fmap (getCohesion . getModality) xs
639 | getCohesion info == defaultCohesion = return $ setCohesion (getCohesion dom) info function
642 let cPi = getCohesion dom -- cohesion of function type
643 let cLam = getCohesion info -- cohesion of lambda
H A DApplication.hs295 typeError $ VariableIsOfUnusableCohesion x (getCohesion a)
395 unless (getCohesion avail `moreCohesion` getCohesion used) $
398 ++ pwords "is used as" ++ [text $ show $ getCohesion used]
399 ++ pwords "but only available as" ++ [text $ show $ getCohesion avail]
H A DDecl.hs580 let c = getCohesion info0
H A DLHS.hs1339 let updCoh = composeCohesion (getCohesion info)
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/
H A DCommon.hs550 getCohesion = modCohesion function
579 getCohesionMod = getCohesion . getModality
1336 getCohesion :: a -> Cohesion
1343 default getCohesion :: LensModality a => a -> Cohesion
1344 getCohesion = modCohesion . getModality function
1350 getCohesion = id function
1385 usableCohesion a = getCohesion a `moreCohesion` Continuous
1689 getCohesion = getCohesionMod function
1883 getCohesion = getCohesionMod function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Concrete/
H A DAttribute.hs166 | getCohesion a == defaultCohesion = Just $ setCohesion c a function
H A DPretty.hs95 if render d == "_" then d else pretty (getCohesion a) <+> d
151 , pretty (getCohesion mod)
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/
H A DEmacsTop.hs414 where c = prettyShow (getCohesion ai)
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/LHS/
H A DUnify.hs1231 if not (getCohesion eqmod `moreCohesion` getCohesion varmod) then return $ UnifyStuck [] else do