Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 -> 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.
tests :: IO BoolSource
Produced by Haddock version 2.6.0