Commits

Branch selector

 master

User selector

jespercockx

Datepicker

All time

Commit History

Commits on Sep 11, 2024

• [ re agda#354 ] Erase type arguments of mapDec

  jespercockx

  committed
  424d31a

Commits on Sep 10, 2024

• [ re agda#354 ] Do not check canonicity of erased instances

  jespercockx

  committed
  a610207

Commits on Sep 7, 2024

• New (simpler but more robust) implementation of canonicity check

  jespercockx

  committed
  03c9aae

Commits on Jul 27, 2024

• Fix typo

  jespercockx

  committed
  7753783

• <$>, <&>, $>, void, and =<< are not class methods

  jespercockx

  committed
  71c06ba

Commits on Jul 26, 2024

• [ re agda#342 ] Proper compilation of projections from tuple records

  jespercockx

  committed
  185dcca

• [ re agda#342 ] Proper compilation of projections from tuple records

  jespercockx

  committed
  b0a185d

• Erase some more predicates in the library

  jespercockx

  committed
  b3e400b

• Add proper import rules for first, second, and (***)

  jespercockx

  committed
  97866ba

• Add @0 annotation to two predicates

  jespercockx

  committed
  66f9cf8

• Move definitions from Prim.Function to Law.Function, delete Prim.Function

  jespercockx

  committed
  c29b0d6

Commits on Jul 24, 2024

• Define Rezz in terms of \exists

  jespercockx

  committed
  83ce549

Commits on Jul 23, 2024

• Remove special handling of tuple types in the prelude

  jespercockx

  committed
  3ca7265

• [ first part of agda#105 ] Add support for compiling records to Haskell tuples

  jespercockx

  committed
  44a82e2

• Whitespace

  jespercockx

  committed
  4e7afa4

Commits on Jul 22, 2024

• [ fix agda#340 ] Compile pattern lambda to regular lambda if all proper patterns are erased

  jespercockx

  committed
  f0bd92a

Commits on Jul 2, 2024

• Avoid double parentheses

  jespercockx

  committed
  f5ac455

• [ fix agda#317 ] Add parens around infix where left argument is another infix with lambda RHS

  jespercockx

  committed
  5f09f42

Commits on Jun 7, 2024

• Add release notes for 1.2 which mysteriously disappeared

  jespercockx

  committed
  9388b77

Commits on May 24, 2024

• [ fix agda#302 ] Move _/=_ function out of the Eq record

  jespercockx

  committed
  7d734a2

Commits on Mar 22, 2024

• [ re agda#305 ] Set the checkpoint in the context of the module rather than the clause

  jespercockx

  committed
  4e66970

• [ re agda#305 ] More robust inlining of indirectly defined instances

  Show description for 50640ad
  jespercockx

  committed
  50640ad

• Some more debug printing for compilation of instances

  jespercockx

  committed
  f49ebac

• Do not drop instance clauses but instead check canonicity

  Show description for 001f845
  jespercockx

  committed
  001f845

• Add missing call to instantiate in compileTerm

  Show description for 060270e
  jespercockx

  committed
  060270e

• [ re agda#305 ] Also set context + checkpoint when checking superclass clauses

  jespercockx

  committed
  1dd0001

• Add some debug printing to compilation of instances

  jespercockx

  committed
  eb7a7e2

• [ fix agda#305 ] Set the module checkpoint when entering the clause body

  jespercockx

  committed
  e8b3b1c

Commits on Mar 13, 2024

• Reinstate check for erasure on type-level lambdas + add todo and test case

  jespercockx

  committed
  f73415a

• [ refactor ] Two small refactorings

  jespercockx

  committed
  1335c39

• [ fix agda#301 ] Already fixed, adding test case

  jespercockx

  committed
  c103bb0

• [ fix agda#264 ] Compile all non-erased module parameters to explicit foralls

  Show description for 3445c36
  jespercockx

  committed
  3445c36

• Allow compilation of hidden parameters to data/record types

  jespercockx

  committed
  ee320df

• Don't use absBody in compileInstanceClause, instead apply to dummy term

  jespercockx

  committed
  9472dfe

• [ refactor ] Remove keepArg function (no longer used)

  jespercockx

  committed
  eb91d15

Pagination

PreviousNext