FreeProving/free-compiler

Issues

• Agda-2.6.* dependency leads to errors

  #225 opened 2 years ago by javiergarea
  0

• cabal.project references use a deprecated git format

  #223 opened 2 years ago by javiergarea
  0

• Adapt Coq examples to the new usability changes

  #164 opened 4 years ago by MarvinLira
  0

• Update Pattern Matching Compiler

  #210 opened 4 years ago by just95
  0

• Instance arguments in sections

  #204 opened 4 years ago by just95
  0

• Translated data types violate Coq's strict positivity restriction

  #155 opened 4 years ago by MajaRet
  0

• Use pure instead of share/call on decreasing argument of fix

  #209 opened 4 years ago by MajaRet
  0

• Rename generated induction schemes from `*_Ind` to `*_ind`

  #163 opened 4 years ago by MarvinLira
  0

• Generate enhanced induction schemes

  #159 opened 4 years ago by MarvinLira
  0

• Add handlers and evaluation strategy to theorems about translated properties

  #202 opened 4 years ago by MajaRet
  0

• Detect effects in functions

  #134 opened 4 years ago by MajaRet
  3

• Generate Normalform instances

  #150 opened 4 years ago by MajaRet
  0

• Generate ShareableArgs instances

  #151 opened 4 years ago by MajaRet
  1

• Sharing in properties produces unprovable Coq propositions

  #211 opened 4 years ago by MajaRet
  0

• Global variables are not shared

  #214 opened 4 years ago by MajaRet
  0

• Type synonym expansion binds type variables not correctly

  #215 opened 4 years ago by MarvinLira
  0

• Implement an analysis of the order of let bindings

  #158 opened 4 years ago by maclement
  0

• Add `call` operator to the lifted IR

  #196 opened 4 years ago by Daniel-Teut
  0

• Handlers induce strictness in proofs

  #208 opened 4 years ago by MajaRet
  0

• Inconsistent sharing behavior for effects in Haskell

  #181 opened 4 years ago by MajaRet
  0

• Synchronize `main` and `dev-case-studies` branch

  #185 opened 4 years ago by MarvinLira
  0

• Allow aliases in decreasing arguments analysis

  #192 opened 4 years ago by just95
  0

• Wrong type is inferred for `let` expressions

  #190 opened 4 years ago by just95
  0

• `let`-bindings don't shadow functions in type inference

  #191 opened 4 years ago by just95
  0

• Implement Handler typeclass

  #177 opened 4 years ago by MajaRet
  0

• Define smart constructors for data types as notations

  #153 opened 4 years ago by MarvinLira
  1

• Replace old effect smart constructors and Partial instances

  #187 opened 4 years ago by MajaRet
  0

• Add a `share` operator to the lifted IR

  #176 opened 4 years ago by Daniel-Teut
  0

• Adapt sharing infrastructure to flexible strategy approach

  #183 opened 4 years ago by MajaRet
  0

• Implement ShareableArgs typeclass

  #149 opened 4 years ago by MajaRet
  0

• Add compiler flag for evaluation strategy

  #168 opened 4 years ago by Daniel-Teut
  0

• Generate simplification lemmas

  #182 opened 4 years ago by MarvinLira
  0

• Implement Normalform typeclass

  #148 opened 4 years ago by MajaRet
  0

• Check whether notation-scopes should be used

  #178 opened 4 years ago by MarvinLira
  1

• Differing type parameters in mutually recursive types produce invalid Coq code

  #172 opened 4 years ago by MajaRet
  0

• Switch from `Ltac` to `Ltac2`

  #165 opened 4 years ago by MarvinLira
  0

• Use lifted IR expression translation in the Coq back end

  #123 opened 4 years ago by JonasHoefer
  0

• Generate induction schemes

  #154 opened 4 years ago by MarvinLira
  0

• Implement polymorphic let bindings

  #157 opened 4 years ago by maclement
  0

• Generate agda-lib file

  #142 opened 4 years ago by JonasHoefer
  0

• Implement type classes for sharing and tracing

  #137 opened 4 years ago by MajaRet
  0

• Translate quick check properties to Agda

  #146 opened 4 years ago by JonasHoefer
  0

• Generate mutual recursive agda data types

  #145 opened 4 years ago by JonasHoefer
  0

• Generate mutual recursive agda functions

  #144 opened 4 years ago by JonasHoefer
  0

• Expand Agda base library

  #121 opened 4 years ago by JonasHoefer
  0

• Built-in operators evaluate arguments in wrong order

  #133 opened 4 years ago by just95
  0

• Construct an effect-generic sharing handler

  #125 opened 4 years ago by MajaRet
  0

• Agda case studies

  #124 opened 4 years ago by JonasHoefer
  0

• Implement a tracing effect in Coq

  #120 opened 4 years ago by MajaRet
  0

• Try out custom simpl lemmas derived from function definitions

  #127 opened 4 years ago by jo-hanna1997
  0