- 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 -> PropertySource
telFromList . telToList == id
prop_flattenTelScope :: TermConfiguration -> PropertySource
All elements of flattenTel
are well-scoped under the original telescope.
prop_flattenTelInv :: TermConfiguration -> PropertySource
unflattenTel . flattenTel == id
prop_reorderTelStable :: TermConfiguration -> PropertySource
reorderTel
is stable.
prop_splitTelescopeScope :: TermConfiguration -> PropertySource
The result of splitting a telescope is well-scoped.
prop_splitTelescopePermScope :: TermConfiguration -> PropertySource
The permutation generated when splitting a telescope preserves scoping.