| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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

tests :: IO Bool | Source

Produced by Haddock version 2.4.2