/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Free/ |
H A D | Precompute.hs | 84 FunSort s1 s2 -> uncurry FunSort <$> precomputeFreeVars (s1, s2)
|
H A D | Reduce.hs | 147 FunSort a b -> FunSort <$> forceNotFree' a <*> forceNotFree' b
|
H A D | Lazy.hs | 553 FunSort s1 s2 -> freeVars' s1 `mappend` freeVars' s2
|
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Internal/ |
H A D | Generic.hs | 135 FunSort a b -> FunSort <$> traverseTermM f a <*> traverseTermM f b 149 FunSort a b -> foldTerm f a <> foldTerm f b
|
H A D | Defs.hs | 85 FunSort s1 s2 -> getDefs s1 >> getDefs s2
|
H A D | MetaVars.hs | 61 sortMetas (FunSort a b) = sortMetas a <> sortMetas b
|
H A D | Names.hs | 140 FunSort a b -> namesIn' sg (a, b)
|
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/ |
H A D | Abstract.hs | 212 FunSort s1 s2 -> FunSort (absS s1) (absS s2) 297 (FunSort a b, FunSort a' b') -> equalSy a a' && equalSy b b'
|
H A D | Irrelevance.hs | 326 FunSort s1 s2 -> usableRel rel (s1,s2) 518 FunSort{} -> False 536 FunSort{} -> False
|
H A D | SyntacticEquality.hs | 119 (FunSort a b, FunSort a' b') -> funSort <$$> synEq a a' <**> synEq' b b'
|
H A D | Conversion.hs | 1260 (FunSort{}, _ ) -> synEq 1261 (_ , FunSort{}) -> synEq 1639 (s1 , FunSort a b) -> funSortEquals s1 a b 1640 (FunSort a b , s2) -> funSortEquals s2 a b 1759 typeError $ UnequalSorts s0 (FunSort s1 s2) 1763 | otherwise -> synEq s0 (FunSort s1 s2) 1778 Nothing -> synEq (Type l) (FunSort s1 $ Type l2) 1795 Nothing -> synEq (Prop l) (FunSort s1 $ Prop l2) 1799 _ -> synEq s0 (FunSort s1 s2)
|
H A D | CheckInternal.hs | 436 FunSort s1 s2 -> do 439 return $ FunSort s1' s2'
|
H A D | Reduce.hs | 339 FunSort s1 s2 -> do 341 maybe (return $ FunSort s1' s2') reduce' $ funSort' s1' s2' 937 FunSort s1 s2 -> funSort <$> simplify' s1 <*> simplify' s2 1085 FunSort s1 s2 -> funSort <$> normalise' s1 <*> normalise' s2 1295 FunSort s1 s2 -> funSort <$> instantiateFull' s1 <*> instantiateFull' s2
|
H A D | Substitute.hs | 835 FunSort s1 s2 -> coerce $ funSort (coerce $ sub s1) (coerce $ sub s2) 1523 isSmallSort FunSort{} = Nothing function 1556 funSort a b = fromMaybe (FunSort a b) $ funSort' a b 1561 piSort' a s1 (NoAbs _ s2) = Just $ FunSort s1 s2 1563 Nothing -> Just $ FunSort s1 $ noabsApp __IMPOSSIBLE__ s2Abs
|
H A D | Quote.hs | 178 quoteSort FunSort{} = pure unsupportedSort
|
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/ |
H A D | Internal.hs | 301 | FunSort (Sort' t) (Sort' t) -- ^ Sort of a (non-dependent) function type. constructor 1121 FunSort s1 s2 -> 1 + tsize s1 + tsize s2 1183 FunSort s1 s2 -> killRange2 FunSort s1 s2 1342 FunSort a b -> mparens (p > 9) $ 1412 FunSort a b -> rnf (a, b)
|
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/MetaVars/ |
H A D | Occurs.hs | 592 FunSort s1 s2 -> FunSort <$> flexibly (occurs s1) <*> flexibly (occurs s2) 612 FunSort s1 s2 -> metaOccurs m (s1,s2) 832 FunSort s1 s2 -> return False
|
H A D | Mention.hs | 59 FunSort s1 s2 -> mentionsMetas xs (s1, s2)
|
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Serialise/Instances/ |
H A D | Internal.hs | 150 icod_ (FunSort a b) = icodeN 5 FunSort a b 166 valu [5, a, b] = valuN FunSort a b
|
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rewriting/ |
H A D | Confluence.hs | 839 FunSort{} -> __IMPOSSIBLE__ 915 FunSort s t -> FunSort <$> metasToVars s <*> metasToVars t
|
H A D | NonLinPattern.hs | 92 FunSort _ _ -> __IMPOSSIBLE__
|
H A D | NonLinMatch.hs | 221 (_ , FunSort{} ) -> matchingBlocked b
|
/dports/math/boolector/boolector-3.2.2/examples/api/python/ |
H A D | api_usage_examples.py | 42 _funsort = b.FunSort([_boolsort, _boolsort, _bvsort, _bvsort], _boolsort)
|
/dports/math/py-pysmt/pysmt-0.9.0/pysmt/solvers/ |
H A D | btor.py | 530 return self._btor.FunSort(stps, rtp)
|
/dports/math/boolector/boolector-3.2.2/doc/ |
H A D | pyboolector.rst | 233 f = btor.UF(btor.FunSort([bv32, bv32], bv8))
|