Home
last modified time | relevance | path

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

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/
H A DAbstract.hs919 nameToExpr :: a -> Expr
924 nameToExpr d =
951 nameToExpr = \case function
953 …DefinedName _ x s -> withSuffix s $ nameToExpr x -- Can be 'isDefName', 'MacroName', 'Quotable…
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DBuiltin.hs706 (v, _t) <- inferExpr (A.nameToExpr x)
890 | Just i <- findBuiltinInfo b -> bindBuiltinInfo i (A.nameToExpr x)
H A DTerm.hs935 Just [n] -> Just (m, FieldAssignment f $ killRange $ A.nameToExpr n)
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Translation/
H A DConcreteToAbstract.hs591 return $ withSuffix suffix $ nameToExpr d