Home
last modified time | relevance | path

Searched refs:debruijnNamedVar (Results 1 – 7 of 7) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Substitute/
H A DDeBruijn.hs13 deBruijnVar = debruijnNamedVar underscore
16 debruijnNamedVar :: String -> Int -> a
17 debruijnNamedVar _ = deBruijnVar function
47 debruijnNamedVar = DBPatVar function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/Builtin/
H A DCoinduction.hs133 ConP sharpCon cpi [ argN $ Named Nothing $ debruijnNamedVar "x" 0 ] ]
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Coverage/
H A DMatch.hs145 debruijnNamedVar n i = toSplitVar (debruijnNamedVar n i) function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A DTelescope.hs112 …med (Just $ WithOrigin Inserted $ unranged $ argNameToString argName) (debruijnNamedVar varName i))
H A DSubstitute.hs1086 debruijnNamedVar n i = varP $ debruijnNamedVar n i function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/
H A DBasicOps.hs1096 pat = [defaultArg $ unnamed $ debruijnNamedVar "c" 0]
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DLHS.hs764 let makeVar = maybe deBruijnVar $ debruijnNamedVar . nameToArgName