Home
last modified time | relevance | path

Searched refs:RewriteRHS (Results 1 – 9 of 9) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DDef.hs458 A.RewriteRHS qes spats rhs wh -> A.RewriteRHS qes spats (mapLHSCores f rhs) wh
689 updateRHS (A.RewriteRHS qes spats rhs wh) =
690 A.RewriteRHS qes (applySubst patSubst spats) (updateRHS rhs) wh
805 A.RewriteRHS eqs ps rhs wh -> rewriteEqnsRHS eqs ps rhs wh
915 | otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
951 handleRHS $ A.RewriteRHS rs strippedPats rhs wh
993 | otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/
H A DAbstract.hs397 | RewriteRHS constructor
417 RewriteRHS a b c d == RewriteRHS a' b' c' d' = and [ a == a', b == b', c == c' , d == d' ] function
703 getRange (RewriteRHS xes _ rhs wh) = getRange (xes, rhs, wh)
847 killRange (RewriteRHS xes spats rhs wh) = killRange4 RewriteRHS xes spats rhs wh
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Abstract/
H A DViews.hs362 RewriteRHS xes spats rhs ds -> RewriteRHS <$> rec xes <*> pure spats <*> rec rhs <*> rec ds
532 RewriteRHS _qes _ rhs cls -> declaredNames rhs <> declaredNames cls
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A DWith.hs237 buildRHS strippedPats1 (A.RewriteRHS qes strippedPats2 rhs wh) =
238 …flip (A.RewriteRHS qes (applySubst withSub $ strippedPats1 ++ strippedPats2)) wh <$> buildRHS [] r…
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/
H A DMakeCase.hs486 rhs@A.RewriteRHS{} -> rhs{ A.rewriteRHS = makeRHSEmptyRecord $ A.rewriteRHS rhs }
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/Highlighting/
H A DFromAbstract.hs319 A.RewriteRHS eqs strippedPats rhs wh -> hl eqs <> hl strippedPats <> hl rhs <> hl wh
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Translation/
H A DInternalToAbstract.hs1066 blank bound (RewriteRHS xes spats rhs _) = __IMPOSSIBLE__ -- NZ
H A DAbstractToConcrete.hs1051 toConcrete (A.RewriteRHS xeqs _spats rhs wh) = do
H A DConcreteToAbstract.hs2642 return $ RewriteRHS eqs [] rhs wh