| /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))
|