List view

[ actions ] move build & html doc deploy to actions

continuous-integration

documentation

Status: Merged (completed).

agda/agda-stdlibnumber 1516

#1516 In agda/agda-stdlib;

· by gallais was closed on Jun 7, 2021

[ Improved fix #1510 ] Get rid of <code>error</code>, use <code>throwError</code> and <code>die</code>.

bug

continuous-integration

Status: Merged (completed).

agda/agda-stdlibnumber 1514

#1514 In agda/agda-stdlib;

· by andreasabel was closed on Jun 3, 2021

[ cleanup ] use modules rather than long names

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 1515

#1515 In agda/agda-stdlib;

· by gallais was closed on Jun 3, 2021

Made <code>Data.Container(.Any/.FreeMonad)</code> safe by splitting out fixed points

breaking

refactoring

safe

sized-types

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Merged (completed).

agda/agda-stdlibnumber 1513

#1513 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Jun 8, 2021

Renamed new <code>Complete</code> list predicate to <code>IsEnumeration</code>

naming

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 1505

#1505 In agda/agda-stdlib;

· by MatthewDaggitt was closed on May 27, 2021

[ Fix #1510 ] Work around GHC bug introduced in 8.2

admin

bug

Status: Merged (completed).

agda/agda-stdlibnumber 1512

#1512 In agda/agda-stdlib;

· by andreasabel was closed on May 31, 2021

[ ci ] doc for the actions script

continuous-integration

documentation

Status: Merged (completed).

agda/agda-stdlibnumber 1522

#1522 In agda/agda-stdlib;

· by gallais was closed on Jun 18, 2021

[ actions ] preserves old HTML doc

bug

continuous-integration

documentation

Status: Merged (completed).

agda/agda-stdlibnumber 1517

#1517 In agda/agda-stdlib;

· by gallais was closed on Jun 7, 2021

Add explicit --guardedness and --sized-types flags

breaking

sized-types

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Merged (completed).

agda/agda-stdlibnumber 1504

#1504 In agda/agda-stdlib;

· by jespercockx was closed on May 24, 2021

Adapt to https://github.com/agda/agda/pull/5289

reflection

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Merged (completed).

agda/agda-stdlibnumber 1453

#1453 In agda/agda-stdlib;

· by jespercockx was closed on Mar 29, 2021

Sized types will no longer be safe in 2.6.2

sized-types

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Merged (completed).

agda/agda-stdlibnumber 1465

#1465 In agda/agda-stdlib;

· by jespercockx was closed on Apr 27, 2021

[ fixed #1484 ] prove m&lt;n⇒m≤1+n by composition ≤-step ∘ &lt;⇒≤

cosmetic

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 1485

#1485 In agda/agda-stdlib;

· by andreasabel was closed on Apr 24, 2021

Define 'pinch' as a counterpart to 'punchIn'

addition

Status: Merged (completed).

agda/agda-stdlibnumber 1492

#1492 In agda/agda-stdlib;

· by TOTBWF was closed on May 6, 2021

Add "Complete" predicate for lists that contain every element of a type

addition

discussion

naming

Status: Merged (completed).

agda/agda-stdlibnumber 1482

#1482 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Apr 29, 2021

Changes related to a change to Agda's reflection machinery.

reflection

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Merged (completed).

agda/agda-stdlibnumber 1480

#1480 In agda/agda-stdlib;

· by nad was closed on Apr 27, 2021

Added weak-induction schemes for <code>Data.Fin</code> and <code>Data.Nat</code>

addition

Status: Merged (completed).

agda/agda-stdlibnumber 1483

#1483 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Apr 28, 2021

Add specialisation of metrics to rational numbers

addition

Status: Merged (completed).

agda/agda-stdlibnumber 1471

#1471 In agda/agda-stdlib;

· by MatthewDaggitt was closed on Apr 22, 2021

[ re #1465 ] Two more modules that are no longer --safe

safe

upstreamChanges induced by Agda upstreamChanges induced by Agda upstream

Status: Merged (completed).

agda/agda-stdlibnumber 1498

#1498 In agda/agda-stdlib;

· by jespercockx was closed on May 7, 2021

Allow ghc-9.0 and test compilation of GenerateEverything on github

admin

Status: Merged (completed).

agda/agda-stdlibnumber 1494

#1494 In agda/agda-stdlib;

· by andreasabel was closed on May 5, 2021

Fast binary conversion

performance

refactoring

Status: Merged (completed).

agda/agda-stdlibnumber 1495

#1495 In agda/agda-stdlib;

· by jmlowenthal was closed on May 12, 2021

Generic traversals of reflected terms

addition

reflection

Status: Merged (completed).

agda/agda-stdlibnumber 1294

#1294 In agda/agda-stdlib;

· by UlfNorell was closed on Sep 28, 2020

Annotated reflected syntax

addition

discussion

Status: Merged (completed).

agda/agda-stdlibnumber 1325

#1325 In agda/agda-stdlib;

· by UlfNorell was closed on Oct 29, 2020

Add Reflection.Universe

addition

reflection

Status: Merged (completed).

agda/agda-stdlibnumber 1324

#1324 In agda/agda-stdlib;

· by UlfNorell was closed on Oct 23, 2020

Bikeshedding #1326: what to do about _⇒_ and ∀[_] on SizedType

discussion

library-design

naming

Status: Merged (completed).

agda/agda-stdlibnumber 1335

#1335 In agda/agda-stdlib;

· by andreasabel was closed on Nov 9, 2020

The 'absurd' pattern now takes a de Bruijn index in reflected syntax

reflection

Status: Merged (completed).

agda/agda-stdlibnumber 1362

#1362 In agda/agda-stdlib;

· by ajrouvoet was closed on Nov 20, 2020