Skip to content

Latest commit

 

History

History
101 lines (79 loc) · 2.74 KB

CHANGELOG.md

File metadata and controls

101 lines (79 loc) · 2.74 KB

Version 1.4-dev

The library has been tested using Agda version 2.6.1.

Highlights

  • First instance modules

Bug-fixes

Non-backwards compatible changes

Deprecated modules

  • Reflection.TypeChecking.MonadSyntax ↦ Reflection.TypeChecking.Monad.Syntax

Deprecated names

Other major additions

  • Instance modules:

    Category.Monad.Partiality.Instances
Codata.Stream.Instances
Codata.Covec.Instances
Data.List.Instances
Data.List.NonEmpty.Instances
Data.Maybe.Instances
Data.Vec.Instances
Function.Identity.Instances

  • Symmetric transitive closures of binary relations:

    Relation.Binary.Construct.Closure.SymmetricTransitive

  • Type-checking monads

    Reflection.TypeChecking.Monad
Reflection.TypeChecking.Monad.Categorical
Reflection.TypeChecking.Monad.Instances

  • Function application in reflected terms (Reflection.Apply)

  • Congruence helper macros in Tactic.Cong

Other major changes

Other minor additions

  • Added proofs to Relation.Binary.PropositionalEquality:

    trans-cong  : trans (cong f p) (cong f q) ≡ cong f (trans p q)
cong₂-reflˡ : cong₂ _∙_ refl p ≡ cong (x ∙_) p
cong₂-reflʳ : cong₂ _∙_ p refl ≡ cong (_∙ u) p

  • Made first argument of [,]-∘-distr in Data.Sum.Properties explicit

  • Added new properties to Data.List.Relation.Binary.Permutation.Propositional.Properties:

    ↭-empty-inv     : xs ↭ [] → xs ≡ []
¬x∷xs↭[]        : ¬ ((x ∷ xs) ↭ [])
↭-singleton-inv : xs ↭ [ x ] → xs ≡ [ x ]
↭-map-inv       : map f xs ↭ ys → ∃ λ ys′ → ys ≡ map f ys′ × xs ↭ ys′
↭-length        : xs ↭ ys → length xs ≡ length ys

  • Added new proofs to ``Data.Sum.Properties`:

    map-id        : map id id ≗ id
map₁₂-commute : map₁ f ∘ map₂ g ≗ map₂ g ∘ map₁ f
[,]-cong      : f ≗ f′ → g ≗ g′ → [ f , g ] ≗ [ f′ , g′ ]
[-,]-cong     : f ≗ f′ → [ f , g ] ≗ [ f′ , g ]
[,-]-cong     : g ≗ g′ → [ f , g ] ≗ [ f , g′ ]
map-cong      : f ≗ f′ → g ≗ g′ → map f g ≗ map f′ g′
map₁-cong     : f ≗ f′ → map₁ f ≗ map₁ f′
map₂-cong     : g ≗ g′ → map₂ g ≗ map₂ g′

  • Added new proofs to Data.Maybe.Relation.Binary.Pointwise:

    nothing-inv : Pointwise R nothing x → x ≡ nothing
just-inv    : Pointwise R (just x) y → ∃ λ z → y ≡ just z × R x z

  • New functions in Reflection.Pattern:

    pattern-size : Pattern → ℕ
pattern-args-size : List (Arg Pattern) → ℕ