Searched refs:ExtendedLam (Results 1 – 14 of 14) sorted by relevance
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Abstract/ |
| H A D | Views.hs | 155 ExtendedLam ei di er x cls -> ExtendedLam ei di er x <$> recurse cls
189 ExtendedLam _ _ _ _ cs -> m `mappend` fold cs
226 ExtendedLam ei di re x cls -> f =<< ExtendedLam ei di re x <$> trav cls
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/ |
| H A D | Abstract.hs | 100 | ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause) constructor
548 ExtendedLam a1 b1 c1 d1 e1 == ExtendedLam a2 b2 c2 d2 e2 = (a1, b1, c1, d1, e1) == function
631 getRange (ExtendedLam i _ _ _ _) = getRange i
762 killRange (ExtendedLam i n e d ps) = killRange5 ExtendedLam i n e d ps
1045 ExtendedLam{} -> __IMPOSSIBLE__
|
| H A D | DoNotation.hs | 114 $ ExtendedLam (getRange cs) -- where-clauses to make highlighting of overlapping
|
| H A D | Concrete.hs | 159 | ExtendedLam Range Erased constructor
811 ExtendedLam r _ _ -> r
1068 killRange (ExtendedLam _ e lrw) = killRange2 (ExtendedLam noRange) e lrw
1185 rnf (ExtendedLam _ a b) = rnf a `seq` rnf b
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Concrete/ |
| H A D | Generic.hs | 121 ExtendedLam r e cs -> f $ ExtendedLam r e $ mapE cs
|
| H A D | Pretty.hs | 190 ExtendedLam _ e pes ->
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/ |
| H A D | Display.hs | 122 A.ExtendedLam{} -> notAllowed "lambdas"
|
| H A D | Term.hs | 1201 A.ExtendedLam i di erased qname cs ->
1304 A.ExtendedLam _ _ _ _ cls -> any hiddenLHS cls
|
| /dports/editors/helix/helix-0.5.0/helix-syntax/languages/tree-sitter-agda/ |
| H A D | parser.y | 680 : '\\' '{' LamClauses '}' { ExtendedLam (getRange ($1,$2,$3,$4)) (reverse $3) }
681 | '\\' 'where' vopen LamWhereClauses close { ExtendedLam (getRange ($1, $2, $4)) (reverse $4) }
688 return $ ExtendedLam (fuseRange $1 es)
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Translation/ |
| H A D | ReflectedToAbstract.hs | 186 (A.ExtendedLam exprNoRange defInfo defaultErased qname cs, es)
|
| H A D | InternalToAbstract.hs | 822 elims (A.ExtendedLam exprNoRange dInfo erased x $
1042 A.ExtendedLam i d e f cs -> A.ExtendedLam i d e f $ blank bound cs
|
| H A D | AbstractToConcrete.hs | 484 A.ExtendedLam{} -> True
799 toConcrete (A.ExtendedLam i di erased qname cs) =
828 C.ExtendedLam (getRange i) erased . List1.fromList <$>
|
| H A D | ConcreteToAbstract.hs | 849 A.ExtendedLam (ExprRange r) di erased qname' $
958 C.ExtendedLam r e cs -> scopeCheckExtendedLam r e cs
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/Highlighting/ |
| H A D | FromAbstract.hs | 252 A.ExtendedLam _r _di _e _q cs -> hl cs -- No hilighting of generated extended lambda name!
|