Home
last modified time | relevance | path

Searched refs:lhsFocus (Results 1 – 4 of 4) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/
H A DAbstract.hs454 , lhsFocus :: NamedArg (LHSCore' e) function
H A DConcrete.hs343 , lhsFocus :: NamedArg LHSCore -- ^ Main argument. function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DApplication.hs1350 , A.lhsFocus = defaultNamedArg $ A.LHSHead c' []
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Translation/
H A DConcreteToAbstract.hs2715 …C.LHSProj{} -> hasExpandedEllipsis $ namedArg $ C.lhsFocus core -- can this ever be Expanded…