Search results

Type synonym expansion binds type variables not correctly

bugSomething isn't workingSomething isn't working

CoqRelated to Coq back end or base libraryRelated to Coq back end or base library

Status: Open.

#215 In FreeProving/free-compiler;

· MarvinLira opened on Sep 27, 2020

Global variables are not shared

DiscussionShould be discussedShould be discussed

Status: Open.

#214 In FreeProving/free-compiler;

· MajaRet opened on Sep 24, 2020

·  

Integrate sharing infrastructure

Sharing in properties produces unprovable Coq propositions

bugSomething isn't workingSomething isn't working

CoqRelated to Coq back end or base libraryRelated to Coq back end or base library

pipelineRelated to the compiler pipeline (e.g. compiler passes or the command line interface)Related to the compiler pipeline (e.g. compiler passes or the command line interface)

Status: Open.

#211 In FreeProving/free-compiler;

· MajaRet opened on Sep 24, 2020

·  

Integrate sharing infrastructure

Handlers induce strictness in proofs

DiscussionShould be discussedShould be discussed

Status: Open.

#208 In FreeProving/free-compiler;

· MajaRet opened on Sep 18, 2020

Generate simplification lemmas

CoqRelated to Coq back end or base libraryRelated to Coq back end or base library

enhancementNew feature or requestNew feature or request

Status: Open.

#182 In FreeProving/free-compiler;

· MarvinLira opened on Sep 1, 2020

Inconsistent sharing behavior for effects in Haskell

HaskellRelated to the Haskell front endRelated to the Haskell front end

Status: Open.

#181 In FreeProving/free-compiler;

· MajaRet opened on Aug 30, 2020

·  

Integrate sharing infrastructure

Differing type parameters in mutually recursive types produce invalid Coq code

bugSomething isn't workingSomething isn't working

CoqRelated to Coq back end or base libraryRelated to Coq back end or base library

Status: Open.

#172 In FreeProving/free-compiler;

· MajaRet opened on Aug 25, 2020

Switch from <code>Ltac</code> to <code>Ltac2</code>

CoqRelated to Coq back end or base libraryRelated to Coq back end or base library

enhancementNew feature or requestNew feature or request

Status: Open.

#165 In FreeProving/free-compiler;

· MarvinLira opened on Jul 31, 2020

Generate enhanced induction schemes

CoqRelated to Coq back end or base libraryRelated to Coq back end or base library

enhancementNew feature or requestNew feature or request

Status: Open.

#159 In FreeProving/free-compiler;

· MarvinLira opened on Jul 28, 2020

Implement polymorphic let bindings

enhancementNew feature or requestNew feature or request

IRChanges of the intermediate representationChanges of the intermediate representation

Status: Open.

#157 In FreeProving/free-compiler;

· maclement opened on Jul 28, 2020

Translated data types violate Coq's strict positivity restriction

bugSomething isn't workingSomething isn't working

CoqRelated to Coq back end or base libraryRelated to Coq back end or base library

Status: Open.

#155 In FreeProving/free-compiler;

· MajaRet opened on Jul 27, 2020

Translate quick check properties to Agda

AgdaRelated to Agda back end or base libraryRelated to Agda back end or base library

Status: Open.

#146 In FreeProving/free-compiler;

· JonasHoefer opened on Jul 22, 2020