| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Substitute/ |
| H A D | Class.hs | 112 idS = IdS
151 liftS k IdS = IdS
162 dropS n IdS = raiseS n
172 composeS rho IdS = rho
173 composeS IdS sgm = sgm function
191 splitS n IdS = (raiseS n, liftS n $ EmptyS impossible)
223 IdS -> deBruijnVar i
224 Wk n IdS -> let j = i + n in
243 listS [] = IdS
264 lazyAbsApp (Abs _ v) u = applySubst (u :# IdS) v -- Note: do not use consS here!
|
| /dports/lang/erlang-runtime22/otp-OTP-22.3.4.24/lib/ssh/src/ |
| H A D | ssh_file.erl | 324 "ecdsa-sha2-"++IdS ->
325 Curve == public_key:ssh_curvename2oid(list_to_binary(IdS));
|
| /dports/lang/erlang-runtime21/otp-OTP-21.3.8.24/lib/ssh/src/ |
| H A D | ssh_file.erl | 324 "ecdsa-sha2-"++IdS ->
325 Curve == public_key:ssh_curvename2oid(list_to_binary(IdS));
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Internal/ |
| H A D | SanityCheck.hs | 37 …IdS -> unless (size gamma == size delta) $ err $ "idS:" <+> hang (pretty gamma <+> "/=") 2 (p…
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/ |
| H A D | LevelConstraints.hs | 58 go _ [] = IdS
|
| H A D | Generalize.hs | 220 (Just IdS, Perm m xs) -> xs == [0 .. m - 1]
221 (Just (Wk n IdS), Perm m xs) -> xs == [0 .. m - n - 1]
387 Wk n IdS -> return (n, _A)
388 IdS -> return (0, _A)
662 recSub = recVal :# Wk i IdS
|
| H A D | DisplayForm.hs | 51 liftLocalDisplayForm IdS df = Just df function
52 liftLocalDisplayForm (Wk n IdS) (Display m lhs rhs) =
|
| H A D | Pretty.hs | 224 prettyTCM IdS = "idS"
225 prettyTCM (Wk m IdS) = "wkS" <+> pretty m
|
| H A D | Substitute.hs | 792 applySubstTerm IdS t = t function
1020 applySubst IdS arg = arg
1030 applySubst IdS dom = dom
1120 applySubst IdS = id
|
| H A D | Coverage.hs | 853 $ checkpoint IdS -- introduce a fresh checkpoint
1052 case (delta1 `abstract` gamma,IdS) of
|
| H A D | Reduce.hs | 1335 IdS -> return IdS
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Reduce/ |
| H A D | Monad.hs | 67 , envCheckpoints = Map.insert chkpt IdS $
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/ |
| H A D | Internal.hs | 631 = IdS
689 empty = IdS
690 null IdS = True
1134 tsize IdS = 1
1190 killRange IdS = IdS
1241 IdS -> "idS"
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/ |
| H A D | Data.hs | 416 (consS iz IdS `composeS` sub params) -- Δ^I ⊢ Δ
426 (consS io IdS `composeS` sub params) -- Δ^I ⊢ Δ
508 (consS iz IdS `composeS` sub params) -- Δ^I ⊢ Δ
780 (consS iz IdS `composeS` sub params) -- Δ^I ⊢ Δ
792 Nothing -> (gamma, IdS, var 1, var 0, map (\ fname -> var 0 `applyProj` unArg fname) fns )
1002 return $ ((theName, gamma, rtype, map (fmap fromLType) clause_types, bodys),IdS)
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/LHS/ |
| H A D | Unify.hs | 875 mempty = UnifyOutput IdS IdS []
881 tellUnifySubst sub = tell $ UnifyOutput sub IdS []
884 tellUnifyProof sub = tell $ UnifyOutput IdS sub []
887 writeUnifyLog x = tell $ UnifyOutput IdS IdS [x]
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Monad/ |
| H A D | Context.hs | 62 $ locallyTC eCheckpoints (const $ Map.singleton 0 IdS)
103 let cps' = Map.insert chkpt IdS $ fmap (applySubst sub) cps
115 , envCheckpoints = Map.insert chkpt IdS $
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Compiler/Treeless/ |
| H A D | Subst.hs | 23 applySubst IdS = id
|
| H A D | Builtin.hs | 138 sub = applySubst (TVar e :# IdS)
|
| H A D | Simplify.hs | 28 runS m = runReader m $ SEnv IdS []
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Serialise/Instances/ |
| H A D | Internal.hs | 546 icod_ IdS = icodeN' IdS
554 valu [] = valuN IdS
|
| /dports/mail/spamassassin/Mail-SpamAssassin-3.4.5/t/data/spam/olevbmacro/ |
| H A D | encrypted.eml | 339 V+nPjY88UEFq7uzNYcBGoRnq3DMG6kZSVWiTFpywAl+zVg1+mbnEexU6L15Jh7v7sJ29/IdS
|
| /dports/mail/spamassassin-devel/spamassassin-1ea352210/t/data/spam/olevbmacro/ |
| H A D | encrypted.eml | 339 V+nPjY88UEFq7uzNYcBGoRnq3DMG6kZSVWiTFpywAl+zVg1+mbnEexU6L15Jh7v7sJ29/IdS
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Coverage/ |
| H A D | Match.hs | 169 applySubst IdS = id
|
| /dports/biology/mummer/mummer-4.0.0beta2-2-g277dac5/src/tigr/ |
| H A D | show-aligns.cc | 214 bool find_sequence(const std::vector<string>& paths, const std::string& IdS, std::string& seq);
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Translation/ |
| H A D | InternalToAbstract.hs | 600 … | Just sub_mtel2local <- msub1 = dropIdentitySubs IdS sub_mtel2local
601 | Just sub_local2mtel <- msub2 = dropIdentitySubs sub_local2mtel IdS
|