Searched refs:telFromList (Results 1 – 25 of 26) sorted by relevance
12
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Internal/ |
| H A D | SanityCheck.hs | 57 dropLast = telFromList . initWithDefault __IMPOSSIBLE__ . telToList
58 dropLastN n = telFromList . dropEnd n . telToList
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/ |
| H A D | Functions.hs | 51 let tel = telFromList ltel
56 let ctel' = telFromList $ telToList ctel ++ ltel
|
| H A D | Telescope.hs | 232 (tel1, tel2) = telFromList -*- telFromList $ splitAt m $ telToList tel'
269 (tel1, tel2) = telFromList -*- telFromList $ splitAt m $ telToList tel'
355 gamma1 = telFromList ts1
356 gamma2' = applyPatSubst rho0 $ telFromList ts2
|
| H A D | DropArgs.hs | 34 dropArgs n tel = telFromList $ drop n $ telToList tel
|
| H A D | Empty.hs | 84 tel = telFromList gamma
|
| H A D | Generalize.hs | 347 pruneMeta (telFromList $ reverse cxt) x
446 let (_Γ, _Δ) = (telFromList gs, telFromList ds)
708 argTel = telFromList $ map hideExplicit $ take nGen $ telToList tel
|
| H A D | Coverage.hs | 989 sctel' = telFromList $ telToList (raise n sctel) ++ telToList tel
1139 …gamma = (fmap . mapModality) (composeModality (getModality info)) $ telFromList . map (fmap prese…
1395 return (fst $ unDom dom, snd <$> dom, telFromList tel1, telFromList tel2)
|
| H A D | Polarity.hs | 276 addContext (telFromList parTel) $ do
|
| H A D | Records.hs | 557 delta = telFromList $ gamma1 ++ telToList tel' ++
558 telToList (applySubst tau0 $ telFromList gamma2)
|
| H A D | Rewriting.hs | 191 inTopContext $ prettyTCM (telFromList delta) <+> " |- " <+> do
|
| H A D | Abstract.hs | 66 tel <- newTelMeta (telFromList $ dropEnd 2 $ telToList eqTel)
|
| H A D | SizedTypes.hs | 219 let tel | n > 0 = telFromList $ drop n $ telToList tel0
|
| H A D | MetaVars.hs | 325 tel' = telFromList $
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/LHS/ |
| H A D | ProblemRest.hs | 34 useNamesFromPattern ps tel = telFromList (zipWith ren ps telList ++ telRemaining)
121 tel = telFromList $ telToList tel0 ++ telToList tel1
|
| H A D | Unify.hs | 787 tel = varTel s `abstract` telFromList (take k $ telToList $ eqTel s)
919 (eqTel1, eqTel2) = (telFromList eqListTel1, telFromList eqListTel2)
1178 | otherwise = telFromList $ zipWith upd (downFrom $ size tel) (telToList tel)
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/ |
| H A D | Display.hs | 64 let dropTel n = telFromList . drop n . telToList
|
| H A D | Record.hs | 663 ptel = telFromList ptelList
|
| H A D | Def.hs | 125 resType = abstract (telFromList (drop (length telList - 1) telList)) tr
618 tel = telFromList (takeLast extra (telToList delta))
|
| H A D | Term.hs | 757 , clauseTel = telFromList [fmap (absurdPatternName,) dom]
1646 delta = telFromList $ drop fvs $ telToList delta0
|
| H A D | Decl.hs | 904 let tel'' = telFromList $ take (size tel' - size etaTel) $ telToList tel'
|
| H A D | Data.hs | 775 gamma' = telFromList $ take (size gamma - 1) $ telToList gamma
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/ |
| H A D | BasicOps.hs | 830 tel <- telFromList . map (fmap (first nameToArgName) . hideButXs) . reverse <$> getContext
1070 reportSDoc "interaction.intro" 10 $ do "introFun" TP.<+> prettyTCM (telFromList tel)
1089 tel' = telFromList [ fmap makeName b | b <- tel ]
1095 let tel = telFromList [defaultDom ("_", t)]
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/ |
| H A D | Internal.hs | 909 telFromList :: ListTel -> Telescope
910 telFromList = telFromList' id function
920 listTel f = fmap telFromList . f . telToList
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Termination/ |
| H A D | Monad.hs | 456 , addContext pars $ prettyTCM (telFromList tel')
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Monad/ |
| H A D | Signature.hs | 87 Just (doms, dom) -> telFromList $ fmap hideOrKeepInstance doms ++ [dom]
|
12