Searched refs:NLPType (Results 1 – 7 of 7) sorted by relevance
76 instance PatternFrom () Type NLPType where78 NLPType <$> patternFrom r k () (getSort a)215 instance NLPatToTerm NLPType Type where216 nlPatToTerm (NLPType s a) = El <$> nlPatToTerm s <*> nlPatToTerm a235 instance NLPatVars NLPType where236 nlPatVarsUnder k (NLPType l a) = nlPatVarsUnder k (l, a)291 instance GetMatchables NLPType where321 instance Free NLPType where322 freeVars' (NLPType s a) =
195 instance Match () NLPType Type where196 match r gamma k _ (NLPType sp p) (El s a) = workOnTypes $ do
255 instance EmbPrj NLPType where256 icod_ (NLPType a b) = icodeN' NLPType a b258 value = valueN NLPType
408 instance PrettyTCM NLPType where409 prettyTCM (NLPType s a) = prettyTCM a
930 instance Subst NLPType where931 type SubstArg NLPType = NLPat932 applySubst rho (NLPType s a) = NLPType (applySubst rho s) (applySubst rho a)
1424 instance InstantiateFull NLPType where1425 instantiateFull' (NLPType s a) = NLPType
1681 | PPi (Dom NLPType) (Abs NLPType)1692 data NLPType = NLPType constructor4532 instance KillRange NLPType where4533 killRange (NLPType s a) = killRange2 NLPType s a4689 instance NFData NLPType