Home
last modified time | relevance | path

Searched +defs:t +defs:tel (Results 1 – 25 of 137) sorted by relevance

123456

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A DTelescope.hs67 tel' = unflattenTel xs tel function
181 varDependents tel = allDependents function
426 -- tel = Γ function
487 pathViewAsPi' t = do function
509 piOrPath t = do function
533 isPath t = either Just (const Nothing) <$> pathViewAsPi t function
556 mustBePi t = ifNotPiType t __IMPOSSIBLE__ $ curry return function
561 ifPi t yes no = do function
583 ifNotPiOrPathType t no yes = do function
611 typeArity t = do function
[all …]
H A DFunctions.hs51 let tel = telFromList ltel function
95 getDef t = reduce t >>= \case function
H A DRecords.hs224 getRecordTypeFields t = do function
254 isRecordType t = either (const Nothing) Just <$> tryRecordType t function
261 tryRecordType t = ifBlocked t (\ m a -> return $ Left $ Blocked m a) $ \ nb t -> do function
532 let tel = recTel def `apply` pars function
556 tel' = mapAbsNames (\ f -> stringToArgName $ argNameToString f ++ "(" ++ s ++ ")") tel function
586 curryAt t n = do function
600 let tel = recTel def `apply` pars function
606 t' = gamma `telePi` (tel `telePi` b') function
659 tel' = apply tel pars function
693 etaExpandAtRecordType t u = do function
[all …]
H A DMetaVars.hs179 let t = telePi_ tel __DUMMY_TYPE__ function
281 let t = telePi_ tel a function
296 newTelMeta tel = newArgsMeta (abstract tel $ __DUMMY_TYPE__) function
325 tel' = telFromList $ function
387 blockTerm t blocker = do function
394 blockTermOnProblem t v pid = do function
474 let t = problemType p function
659 let t = jMetaType $ mvJudgement mvar function
1180 t = jMetaType $ mvJudgement m function
1265 t' = telePi tel size function
[all …]
H A DProjectionLike.hs245 let t = defType defn function
296 tel = take pIndex $ telToList $ theTel $ telView' t function
H A DSizedTypes.hs53 checkSizeLtSat t = whenM haveSizeLt $ do function
219 let tel | n > 0 = telFromList $ drop n $ telToList tel0 function
720 tel = replicate ar $ defaultArg "s" function
/dports/audio/re/re-0.5.8/src/telev/
H A Dtelev.c134 struct telev *t = arg; in destructor() local
150 struct telev *t; in telev_alloc() local
189 int telev_set_srate(struct telev *tel, uint32_t srate) in telev_set_srate()
209 int telev_send(struct telev *tel, int event, bool end) in telev_send()
240 int telev_recv(struct telev *tel, struct mbuf *mb, int *event, bool *end) in telev_recv()
282 int telev_poll(struct telev *tel, bool *marker, struct mbuf *mb) in telev_poll()
/dports/x11-fonts/psftools/psftools-1.0.13/winfonts/
H A Dmz.c19 long tel; in new_MZFILE() local
65 long off, t; in mz_type() local
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Telescope/
H A DPath.hs80 telePiPath_ tel t bndry = do function
93 arityPiPath t = do function
111 isInterval t = liftTCM $ do function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DDecl.hs356 [ " t = " <+> prettyTCM t function
357 , " t' = " <+> prettyTCM t' function
833 tel = absBody btel in function
897 let tel' = apply tel vs function
904 let tel'' = telFromList $ take (size tel' - size etaTel) $ telToList tel' function
945 let tel = tel' `apply` vs function
H A DRecord.hs99 let tel = abstract gtel ptel function
115 -- t = tel -> t0 where t0 must be a sort s function
470 t = s `applyPatSubst` rtype function
599 -- tel = {A' : Set} {B' : Set} (r : Prod A' B') function
616 let t' = raiseFrom (size ftel1) 1 t function
617 t'' = applySubst (parallelS vs) t' function
H A DData.hs89 let tel = abstract gtel ptel function
90 tel' = hideAndRelParams <$> tel function
91 -- let tel' = hideTel tel function
177 forceSort t = reduce (unEl t) >>= \case function
661 fromCType (LType t) = fromLType t function
862 t = ExtendTel (defaultDom $ raise (size tel) int) (Abs "i" EmptyTel) function
1015 bindGeneralizedParameters [] t ret = ret EmptyTel t function
1202 let t' = El (raise n $ dataSort $ theDef def) $ Def q $ map Apply $ us ++ xs function
1227 isCoinductive t = do function
/dports/multimedia/libv4l/linux-5.13-rc2/net/ipv6/
H A Dip6_tunnel.c118 struct ip6_tnl *t, *cand = NULL; in ip6_tnl_lookup() local
291 struct ip6_tnl *t; in ip6_tnl_create() local
346 struct ip6_tnl *t; in ip6_tnl_locate() local
436 struct ipv6_tlv_tnl_enc_lim *tel; in ip6_tnl_parse_tlv_enc_lim() local
473 struct ip6_tnl *t; in ip6_tnl_err() local
508 struct ipv6_tlv_tnl_enc_lim *tel; in ip6_tnl_err() local
920 struct ip6_tnl *t; in ipxip6_rcv() local
1330 struct ipv6_tlv_tnl_enc_lim *tel; in ipxip6_tnl_xmit() local
2029 struct ip6_tnl *nt, *t; in ip6_tnl_newlink() local
2229 struct ip6_tnl *t; in ip6_tnl_destroy_tunnels() local
[all …]
H A Dip6_gre.c123 struct ip6_tnl *t, *cand = NULL; in ip6gre_tunnel_lookup() local
286 struct ip6_tnl *t) in ip6erspan_tunnel_unlink_md()
293 const struct ip6_tnl *t) in ip6gre_bucket()
329 struct ip6_tnl *t; in ip6gre_tunnel_find() local
349 struct ip6_tnl *t, *nt; in ip6gre_tunnel_locate() local
400 struct ip6_tnl *t = netdev_priv(dev); in ip6erspan_tunnel_uninit() local
429 struct ip6_tnl *t; in ip6gre_err() local
456 struct ipv6_tlv_tnl_enc_lim *tel; in ip6gre_err() local
676 struct ipv6_tlv_tnl_enc_lim *tel; in prepare_ip6gre_xmit_ipv6() local
1564 struct ip6_tnl *t; in ip6gre_destroy_tunnels() local
[all …]
/dports/multimedia/v4l_compat/linux-5.13-rc2/net/ipv6/
H A Dip6_tunnel.c118 struct ip6_tnl *t, *cand = NULL; in ip6_tnl_lookup() local
291 struct ip6_tnl *t; in ip6_tnl_create() local
346 struct ip6_tnl *t; in ip6_tnl_locate() local
436 struct ipv6_tlv_tnl_enc_lim *tel; in ip6_tnl_parse_tlv_enc_lim() local
473 struct ip6_tnl *t; in ip6_tnl_err() local
508 struct ipv6_tlv_tnl_enc_lim *tel; in ip6_tnl_err() local
920 struct ip6_tnl *t; in ipxip6_rcv() local
1330 struct ipv6_tlv_tnl_enc_lim *tel; in ipxip6_tnl_xmit() local
2029 struct ip6_tnl *nt, *t; in ip6_tnl_newlink() local
2229 struct ip6_tnl *t; in ip6_tnl_destroy_tunnels() local
[all …]
H A Dip6_gre.c123 struct ip6_tnl *t, *cand = NULL; in ip6gre_tunnel_lookup() local
286 struct ip6_tnl *t) in ip6erspan_tunnel_unlink_md()
293 const struct ip6_tnl *t) in ip6gre_bucket()
329 struct ip6_tnl *t; in ip6gre_tunnel_find() local
349 struct ip6_tnl *t, *nt; in ip6gre_tunnel_locate() local
400 struct ip6_tnl *t = netdev_priv(dev); in ip6erspan_tunnel_uninit() local
429 struct ip6_tnl *t; in ip6gre_err() local
456 struct ipv6_tlv_tnl_enc_lim *tel; in ip6gre_err() local
676 struct ipv6_tlv_tnl_enc_lim *tel; in prepare_ip6gre_xmit_ipv6() local
1564 struct ip6_tnl *t; in ip6gre_destroy_tunnels() local
[all …]
/dports/multimedia/v4l-utils/linux-5.13-rc2/net/ipv6/
H A Dip6_tunnel.c118 struct ip6_tnl *t, *cand = NULL; in ip6_tnl_lookup() local
291 struct ip6_tnl *t; in ip6_tnl_create() local
346 struct ip6_tnl *t; in ip6_tnl_locate() local
436 struct ipv6_tlv_tnl_enc_lim *tel; in ip6_tnl_parse_tlv_enc_lim() local
473 struct ip6_tnl *t; in ip6_tnl_err() local
508 struct ipv6_tlv_tnl_enc_lim *tel; in ip6_tnl_err() local
920 struct ip6_tnl *t; in ipxip6_rcv() local
1330 struct ipv6_tlv_tnl_enc_lim *tel; in ipxip6_tnl_xmit() local
2029 struct ip6_tnl *nt, *t; in ip6_tnl_newlink() local
2229 struct ip6_tnl *t; in ip6_tnl_destroy_tunnels() local
[all …]
H A Dip6_gre.c123 struct ip6_tnl *t, *cand = NULL; in ip6gre_tunnel_lookup() local
286 struct ip6_tnl *t) in ip6erspan_tunnel_unlink_md()
293 const struct ip6_tnl *t) in ip6gre_bucket()
329 struct ip6_tnl *t; in ip6gre_tunnel_find() local
349 struct ip6_tnl *t, *nt; in ip6gre_tunnel_locate() local
400 struct ip6_tnl *t = netdev_priv(dev); in ip6erspan_tunnel_uninit() local
429 struct ip6_tnl *t; in ip6gre_err() local
456 struct ipv6_tlv_tnl_enc_lim *tel; in ip6gre_err() local
676 struct ipv6_tlv_tnl_enc_lim *tel; in prepare_ip6gre_xmit_ipv6() local
1564 struct ip6_tnl *t; in ip6gre_destroy_tunnels() local
[all …]
/dports/astro/oskar/OSKAR-2.8.0/oskar/vis/src/
H A Doskar_vis_block_add_system_noise.c17 double frequency_hz, const oskar_Telescope* tel, int* status) in oskar_get_station_std_dev_for_channel()
237 int t = 0, c = 0; in oskar_vis_block_add_system_noise() local
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rewriting/
H A DNonLinMatch.hs170 let t' = absApp b (unArg v) function
177 t' = b `absApp` u function
285 tel = permuteTel perm k function
291 let t' = telePi tel $ renameP impossible perm t function
/dports/sysutils/k3b/k3b-21.12.3/libk3b/projects/videocd/
H A Dk3bvcdjob.cpp315 QDomText tel = el.firstChild().toText(); in slotParseVcdxBuildOutput() local
454 void K3b::VcdJob::slotWriterNextTrack( int t, int tt ) in slotWriterNextTrack()
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Termination/
H A DMonad.hs287 terSetTarget t = terLocal $ \ e -> e { terTarget = t } function
446 (pars, tel') = splitAt n $ telToList tel function
606 terSetSizeDepth tel cont = do function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/
H A DBasicOps.hs123 let t = case mvJudgement mv of function
1089 tel' = telFromList [ fmap makeName b | b <- tel ] function
1095 let tel = telFromList [defaultDom ("_", t)] function
1232 tel = apply rtel vs function
1239 , " tel = " TP.<+> prettyTCM tel function
H A DMakeCase.hs225 recheckAbstractClause t sub acl = checkClauseLHS t sub acl $ \ lhs -> do function
272 tel = clauseTel clause function
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Monad/
H A DSignature.hs79 let tel' = replaceEmptyName "r" $ killRange $ case theDef d of function
446 t = defType d `piApply` ts' function
558 tel = Ξ.(Θ.Δ)[ts] function
570 tel = Θ.Γ.Φ (section Top.A.M) function
574 tel = Θ₂.Γ.Φ[ts'] function

123456