Searched refs:reAbs (Results 1 – 3 of 3) sorted by relevance
35 telePiPath reAbs lams tel t bs = do function68 return $ El (mkPiSort a b) (Pi a (reAbs b))
280 reAbs :: (Subst a, Free a) => Abs a -> Abs a281 reAbs (NoAbs x v) = NoAbs x v function282 reAbs (Abs x v) = mkAbs x v function
1260 telePi' reAbs = telePi where function1262 telePi (ExtendTel u tel) t = el $ Pi u $ reAbs b1269 telePi = telePi' reAbs1288 b' = reAbs b