Searched refs:DataOrRecSig (Results 1 – 23 of 23) sorted by relevance
188 DataOrRecSig{} -> True328 DataOrRecSig{} -> reportSLn "tc.proj.like" 30 $ " not a function, but DataOrRecSig"
97 DataOrRecSig{} -> yes239 DataOrRecSig{} -> True
251 DataOrRecSig{} -> False577 DataOrRecSig{} -> mempty
301 DataOrRecSig n -> DataOrRecSig (n - length args)652 DataOrRecSig n -> DataOrRecSig (size tel + n)
322 DataOrRecSig{} -> pure agdaDefinitionPostulate
1459 DataOrRecSig{} -> return d
49 DataOrRecSig{} -> no
453 DataOrRecSig{} -> __IMPOSSIBLE__
86 DataOrRecSig{} -> mempty
646 DataName -> DataOrRecSig npars647 RecName -> DataOrRecSig npars
91 DataOrRecSig n -> n
72 DataOrRecSig n -> n1234 DataOrRecSig{} -> return Nothing
379 DataOrRecSig{} -> return ()1527 DataOrRecSig{} -> hardTypeError . GenericDocError =<< do
661 DataOrRecSig{} -> True
1077 makeAbs d@DataOrRecSig{} = Just d1164 DataOrRecSig{} -> 0
2007 | DataOrRecSig constructor2162 pretty (DataOrRecSig n) = "DataOrRecSig" <+> pretty n2494 DataOrRecSig{} -> ConcreteDef2508 DataOrRecSig{} -> []4569 DataOrRecSig n -> DataOrRecSig n
274 defnToKind TCM.DataOrRecSig{} = Postulate
380 DataOrRecSig{} -> __IMPOSSIBLE__
376 icod_ DataOrRecSig{} = __IMPOSSIBLE__
548 metaOccurs m DataOrRecSig{} = return ()
119 MB.DataOrRecSig{} -> return (Postulate, [])
818 DataOrRecSig{} -> True
148 DataOrRecSig{} -> pure CAxiom