Searched refs:dataIxs (Results 1 – 5 of 5) sorted by relevance
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Compiler/MAlonzo/ |
| H A D | Compiler.hs | 470 Datatype{ dataPars = np, dataIxs = ni, dataClause = cl }
485 Datatype{ dataPars = np, dataIxs = ni, dataClause = cl } -> do
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/ |
| H A D | Data.hs | 143 , dataIxs = nofIxs function
|
| H A D | Builtin.hs | 989 , dataIxs = 0 function
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Monad/ |
| H A D | Base.hs | 2056 , dataIxs :: Nat -- ^ Number of indices. function
2182 , "dataIxs =" <?> pshow dataIxs
|
| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Primitive/ |
| H A D | Cubical.hs | 1024 Datatype{dataPars = pars, dataIxs = ixs, dataPathCons = pcons}
|