Searched refs:LensLock (Results 1 – 3 of 3) sorted by relevance
60 type LensAttribute a = (LensRelevance a, LensQuantity a, LensCohesion a, LensLock a)171 setPristineLock :: (LensLock a) => Lock -> a -> Maybe a
1278 class LensLock a where constructor1288 instance LensLock Lock where1293 instance LensLock ArgInfo where1297 instance LensLock (Arg t) where
318 checkDomain :: (LensLock a, LensModality a) => LamOrPi -> List1 a -> A.Expr -> TCM Type347 checkPiDomain :: (LensLock a, LensModality a) => List1 a -> A.Expr -> TCM Type