| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/ |
| H A D | Substitute.hs | 507 Branches cop (applyE cs es) (second (`applyE` es) <$> eta)(applyE ls es) (applyE m es) b lz
522 applyE (DTerm v) es = DTerm $ applyE v es function
523 applyE (DDot v) es = DDot $ applyE v es function
531 applyE ts es = map (`applyE` es) ts function
535 applyE b es = fmap (`applyE` es) b function
539 applyE x es = fmap (`applyE` es) x function
543 applyE x es = fmap (`applyE` es) x function
547 applyE x es = fmap (`applyE` es) x function
551 applyE x es = fmap (`applyE` es) x function
555 applyE (x,y) es = (applyE x es , applyE y es ) function
[all …]
|
| H A D | Reduce.hs | 161 inst = applySubst rho (foldr mkLam v $ drop (length es1) tel) `applyE` es2
166 BlockedConst u | blocking -> instantiate' . unBrave $ BraveTerm u `applyE` es
416 IZero -> red (applyE x es)
417 IOne -> red (applyE y es)
552 v = v0 `applyE` es
600 noReduction $ applyE (Def f []) <$> do
604 YesReduction simpl v -> yesReduction simpl $ v `applyE` es2
628 vfull = v0 `applyE` map ignoreReduced es
778 [] -> rewrite (NotBlocked MissingClauses ()) (applyE v) rewr es
791 DontKnow b -> rewrite b (applyE v) rewr es
[all …]
|
| H A D | CheckInternal.hs | 383 inferSpine' action (b `absApp` r) (self `applyE` [e]) (self' `applyE` [IApply x' y' r']) es
388 inferSpine' action (b `absApp` v) (self `applyE` [e]) (self' `applyE` [Apply (Arg ai v')]) es
|
| H A D | DisplayForm.hs | 37 dtermToTerm d `apply` map (defaultArg . dtermToTerm) ds `applyE` es
134 return (d, substWithOrigin (parallelS $ map woThing us) us v `applyE` es1)
|
| H A D | Records.hs | 390 (ArgT a :) <$> typeElims (absApp b $ unArg v) (self `applyE` [e]) es
682 let xs' = for (map argFromDom xs) $ fmap $ \ x -> u `applyE` [Proj ProjSystem x]
837 isEtaVarG (u `applyE` [Proj o f]) fa mi (es ++ [Proj o f])
861 areEtaVarElims (u `applyE` [Proj o f]) fa es es'
|
| H A D | RecordPatterns.hs | 78 proj p = (`applyE` [Proj ProjSystem $ unDom p])
770 let proj p = (`applyE` [Proj ProjSystem $ unDom p])
|
| H A D | Sort.hs | 215 hd' <- applyE <$> applyDef o f (argFromDom b $> hd [])
|
| H A D | ReconstructParameters.hs | 183 Just pr -> return $ applyE (projDropPars pr ProjSystem) vs
|
| H A D | ProjectionLike.hs | 177 ProjectionView f a es -> (`applyE` (Proj ProjPrefix f : es)) <$> elimView pe (unArg a)
|
| H A D | Coverage.hs | 438 … , clauseBody = (`applyE` patternsToElims extra) . (s `applyPatSubst`) <$> clauseBody cl
817 rhs <- pure $ raise n rhs `applyE` teleElims deltaEx bs
1604 let self = defaultArg $ Def f [] `applyE` es
1606 fieldValues = for fs $ \ proj -> unArg self `applyE` [Proj ProjSystem (unDom proj)]
|
| H A D | Conversion.hs | 238 let w = u `applyE` es
346 … let (m',n') = raise 1 (m, n) `applyE` [IApply (raise 1 $ unArg x) (raise 1 $ unArg y) (var 0)]
821 let v1 = applyE v els01
822 v2 = applyE v els02
867 (applyE v [e]) els1 els2
|
| H A D | Rewriting.hs | 442 Right w -> return $ YesReduction YesSimplification $ w `applyE` es2
|
| H A D | With.hs | 559 strip (self `applyE` e) t' ps qs
|
| /dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/_cabal_deps/ghc-exactprint-0.6.4/tests/examples/ghc84/ |
| H A D | Types.hs | 24 , applyE
128 applyE :: (el1 -> el2 -> el) -> Editor in_ el1 (a -> b) -> Editor in_ el2 a -> Editor in_ el b
129 applyE combineElements a b = Editor $ \s -> do function
142 (<<*>>) = applyE ($)
146 (<*>) = applyE mappend
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/CompiledClause/ |
| H A D | Match.hs | 77 | otherwise -> yes $ applySubst (toSubst es0) t `applyE` map ignoreReduced es1
92 …let projs = [ MaybeRed NotReduced $ Apply $ Arg ai $ relToDontCare ai $ v0 `applyE` [Proj ProjSyst…
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Substitute/ |
| H A D | Class.hs | 26 applyE :: t -> Elims -> t
28 apply t args = applyE t $ map Apply args
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rewriting/ |
| H A D | Confluence.hs | 239 let rhs1 = applySubst sub1 (rewRHS rew1) `applyE` es2r
240 rhs2 = applySubst sub2 (rewRHS rew2) `applyE` es1r
322 let w = applySubst sub2 (rewRHS rew2) `applyE` es1r
570 let w = (applySubst sub' rhs) `applyE` es1'
789 hd' <- applyE <$> applyDef o f (argFromDom b $> hd [])
|
| H A D | NonLinMatch.hs | 178 hd' <- addContext k $ applyE <$> applyDef o f (argFromDom a $> u)
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/ |
| H A D | Application.hs | 269 mapFst applyE <$> inferDef app x
297 return (applyE u, unDom a)
323 return (applyE u . drop n, a)
329 return (applyE term, t)
1194 v <- checkHeadConstraints (u `applyE`) st
1202 v <- checkHeadConstraints (u `applyE`) st
|
| H A D | Record.hs | 433 let project = (\ t fn -> t `applyE` [Proj ProjSystem fn])
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Primitive/ |
| H A D | Base.hs | 118 pure $ t `applyE` [IApply x y r]
|
| H A D | Cubical.hs | 182 pure $ p `applyE` [IApply x y i]
561 t1' o = t1'alpha o <&> (`applyE` [Proj ProjSystem (sigmaFst kit)])
562 alpha o = t1'alpha o <&> (`applyE` [Proj ProjSystem (sigmaSnd kit)])
741 t1' o = t1'alpha o <&> (`applyE` [Proj ProjSystem (sigmaFst kit)])
742 alpha o = t1'alpha o <&> (`applyE` [Proj ProjSystem (sigmaSnd kit)])
910 t1' o = t1'alpha o <&> (`applyE` [Proj ProjSystem (sigmaFst kit)])
911 alpha o = t1'alpha o <&> (`applyE` [Proj ProjSystem (sigmaSnd kit)])
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Patterns/ |
| H A D | Match.hs | 238 matchPatterns ps $ for fs $ \ (Arg ai f) -> Arg ai $ v `applyE` [Proj ProjSystem f]
|
| /dports/devel/stack/stack-2.7.3/_cabal_deps/persistent-2.13.0.1/Database/Persist/ |
| H A D | TH.hs | 1584 applyE <- [|(<*>)|]
1585 let applyFromPersistValue = infixFromPersistValue applyE
1591 infixFromPersistValue applyE fpv exp name =
1592 UInfixE exp applyE (fpv `AppE` VarE name)
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Reduce/ |
| H A D | Fast.hs | 716 return $ applyE (applySubst (parS vs) t) es <$ b
1329 case runReduce (rewrite blk (applyE v0) rewr es) of
|