Searched refs:defAbstract (Results 1 – 12 of 12) sorted by relevance
153 , defAbstract :: IsAbstract179 lensIsAbstract f i = (f $! defAbstract i) <&> \ a -> i { defAbstract = a }182 anyIsAbstract = defAbstract
904 anyAbstract (Axiom _ i _ _ _ _) = defAbstract i == AbstractDef905 anyAbstract (Field i _ _) = defAbstract i == AbstractDef909 anyAbstract (FunDef i _ _ _) = defAbstract i == AbstractDef910 anyAbstract (DataDef i _ _ _ _) = defAbstract i == AbstractDef911 anyAbstract (RecDef i _ _ _ _ _ _) = defAbstract i == AbstractDef912 anyAbstract (DataSig i _ _ _) = defAbstract i == AbstractDef913 anyAbstract (RecSig i _ _ _) = defAbstract i == AbstractDef
520 whenAbstractFreezeMetasAfter Info.DefInfo{ defAccess, defAbstract} m = do521 if defAbstract /= AbstractDef then m else do644 FunName -> emptyFunction{ funAbstr = Info.defAbstract i }645 MacroName -> set funMacro True emptyFunction{ funAbstr = Info.defAbstract i }712 Primitive { primAbstr = Info.defAbstract i794 | Info.defAbstract i == AbstractDef -> inConcreteMode
222 , recAbstr = Info.defAbstract i241 , conAbstr = Info.defAbstract i579 , "abstr =" <+> (text . show) (Info.defAbstract info)
30 import Agda.Syntax.Info hiding (defAbstract)93 | Info.defAbstract i /= AbstractDef ->200 , funAbstr = Info.defAbstract i415 , funAbstr = Info.defAbstract i1180 abstr <- defAbstract <$> ignoreAbstractMode (getConstInfo f)
147 , dataAbstr = Info.defAbstract i265 comp <- if nofIxs /= 0 || (Info.defAbstract i == AbstractDef)279 , conAbstr = Info.defAbstract i
805 [ text $ show $ A.defAbstract di817 abstract (A.defAbstract di) $ do
801 a = defAbstract info
421 … y <+> "from" <+> pretty x <+> "with" <+> text (show np) <+> "args" <+> text (show $ defAbstract d)1067 case defAbstract d of1113 case defAbstract def of
2491 defAbstract :: Definition -> IsAbstract2492 defAbstract d = case theDef d of function
501 let a = defAbstract def
505 . abst (A.defAbstract i)