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

Agda.TypeChecking.Tests

Contents

Synopsis

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_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.