| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.TypeChecking.Tests
- prop_telToListInv :: TermConfiguration -> Property
- prop_flattenTelScope :: TermConfiguration -> Property
- prop_flattenTelInv :: TermConfiguration -> Property
- prop_reorderTelStable :: TermConfiguration -> Property
- prop_splitTelescopeScope :: TermConfiguration -> Property
- prop_splitTelescopePermScope :: TermConfiguration -> Property
- tests :: IO Bool
Tests for Agda.Utils.Permutation
Tests for Agda.TypeChecking.Telescope
prop_telToListInv :: TermConfiguration -> Property Source
telFromList . telToList == id
prop_flattenTelScope :: TermConfiguration -> Property Source
All elements of flattenTel are well-scoped under the original telescope.
prop_flattenTelInv :: TermConfiguration -> Property Source
unflattenTel . flattenTel == id
prop_reorderTelStable :: TermConfiguration -> Property Source
reorderTel is stable.
prop_splitTelescopeScope :: TermConfiguration -> Property Source
The result of splitting a telescope is well-scoped.
prop_splitTelescopePermScope :: TermConfiguration -> Property Source
The permutation generated when splitting a telescope preserves scoping.