Searched refs:projLams (Results 1 – 9 of 9) sorted by relevance
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/Builtin/ |
| H A D | Coinduction.hs | 148 , projLams = ProjLams $ [ argH "a" , argH "A" , argN "x" ] function
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/ |
| H A D | ProjectionLike.hs | 303 , projLams = ProjLams $ map (argFromDom . fmap fst) tel function
|
| H A D | Substitute.hs | 289 , projLams = projLams p `apply` args function
639 , projLams = abstract tel $ projLams p function
|
| H A D | Generalize.hs | 773 , projLams = ProjLams [defaultArg "gtel"] } in function
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/ |
| H A D | Record.hs | 695 , projLams = ProjLams $ map (argFromDom . fmap fst) telList function
|
| H A D | Data.hs | 609 , projLams = ProjLams $ map (argFromDom . fmap fst) $ telToList projTel function
|
| H A D | LHS.hs | 1683 when (null $ projLams proj) $ wrongProj d
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Monad/ |
| H A D | Signature.hs | 486 , projLams = projLams p `apply` ts' function
|
| H A D | Base.hs | 1931 , projLams :: ProjLams function
2228 , "projLams =" <?> pretty projLams
|