defaultDefn (reference) in projects: dports

Project(s)

Full Search
Definition
Symbol
File Path
History
Type

Searched refs:defaultDefn (Results 1 – 12 of 12) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A D	Record.hs	214 defaultDefn defaultArgInfo name t $ 235 defaultDefn defaultArgInfo conName (telh `abstract` contype) $ 720 (defaultDefn ai projname (killRange finalt)
H A D	Data.hs	`154 defaultDefn defaultArgInfo name t dataDef 170 defaultDefn defaultArgInfo name t $ 274 defaultDefn ai c (telePi tel t) $ Constructor 615 (defaultDefn defaultArgInfo projName (unDom projType) fun) 742 noMutualBlock $ addConstant theName $ (defaultDefn defaultArgInfo theName theType 908 noMutualBlock $ addConstant theName $ (defaultDefn defaultArgInfo theName theType`
H A D	Builtin.hs	`930 addConstant q $ defaultDefn (setRelevance rel defaultArgInfo) q t def 957 addConstant q $ defaultDefn defaultArgInfo q t def 978 addConstant q $ defaultDefn defaultArgInfo q t def 984 addConstant q $ defaultDefn defaultArgInfo q t (def t) 1007 addConstant q $ defaultDefn defaultArgInfo q (sort $ univSort s) def`
H A D	Def.hs	`181 addConstant name $ defaultDefn ai name t 422 defaultDefn ai name fullType defn 1066 useTerPragma $ defaultDefn defaultArgInfo aux __DUMMY_TYPE__ emptyFunction 1160 useTerPragma $ (defaultDefn defaultArgInfo aux withFunType emptyFunction)`
H A D	Decl.hs	`551 addConstant x $ (defaultDefn info x tGen GeneralizableVar) 642 let defn = defaultDefn info x t $ 711 defaultDefn info x t $`
H A D	Term.hs	`749 (\ d -> (defaultDefn (setModality mod info') aux t' d) 822 (defaultDefn info qname t emptyFunction) { defMutual = j }`
H A D	Application.hs	`1364 (defaultDefn ai c' forcedType emptyFunction)`
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A D	Generalize.hs	`768 addConstant field $ defaultDefn (getArgInfo fld) field fieldTy $ 789 …addConstant (conName genRecCon) $ defaultDefn defaultArgInfo (conName genRecCon) __DUMMY_TYPE__ $ … 803 addConstant genRecName $ defaultDefn defaultArgInfo genRecName (sort genRecSort) $`
H A D	Abstract.hs	`139 noMutualBlock $ addConstant hole $ defaultDefn defaultArgInfo hole a defaultAxiom`
H A D	Unquote.hs	`888 addConstant x $ defaultDefn i x a emptyFunction 909 addConstant x $ defaultDefn i x a defaultAxiom`
H A D	MetaVars.hs	`1579 addConstant q $ defaultDefn defaultArgInfo q t defaultAxiom`
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Monad/
H A D	Base.hs	`1820 defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition 1821 defaultDefn info x t def = Defn function`