Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Tests

Contents

- Tests for Agda.Utils.Permutation
- Tests for Agda.TypeChecking.Telescope

Synopsis

- 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

    telFromList . telToList == id

prop_flattenTelScope :: TermConfiguration -> Property

All elements of `flattenTel` are well-scoped under the original telescope.

prop_flattenTelInv :: TermConfiguration -> Property

    unflattenTel . flattenTel == id

prop_reorderTelStable :: TermConfiguration -> Property

`reorderTel` is stable.

prop_splitTelescopeScope :: TermConfiguration -> Property

The result of splitting a telescope is well-scoped.

prop_splitTelescopePermScope :: TermConfiguration -> Property

The permutation generated when splitting a telescope preserves scoping.

tests :: IO Bool