-
Notifications
You must be signed in to change notification settings - Fork 3
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
Type synonym expansion binds type variables not correctly
bugSomething isn't workingSomething isn't workingCoqRelated to Coq back end or base libraryRelated to Coq back end or base libraryStatus: Open.#215 In FreeProving/free-compiler;Global variables are not shared
DiscussionShould be discussedShould be discussedStatus: Open.Sharing in properties produces unprovable Coq propositions
bugSomething isn't workingSomething isn't workingCoqRelated to Coq back end or base libraryRelated to Coq back end or base librarypipelineRelated 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.Handlers induce strictness in proofs
DiscussionShould be discussedShould be discussedStatus: Open.#208 In FreeProving/free-compiler;Generate simplification lemmas
CoqRelated to Coq back end or base libraryRelated to Coq back end or base libraryenhancementNew feature or requestNew feature or requestStatus: Open.#182 In FreeProving/free-compiler;Inconsistent sharing behavior for effects in Haskell
HaskellRelated to the Haskell front endRelated to the Haskell front endStatus: Open.Differing type parameters in mutually recursive types produce invalid Coq code
bugSomething isn't workingSomething isn't workingCoqRelated to Coq back end or base libraryRelated to Coq back end or base libraryStatus: Open.#172 In FreeProving/free-compiler;Switch from
LtactoLtac2CoqRelated to Coq back end or base libraryRelated to Coq back end or base libraryenhancementNew feature or requestNew feature or requestStatus: Open.#165 In FreeProving/free-compiler;Generate enhanced induction schemes
CoqRelated to Coq back end or base libraryRelated to Coq back end or base libraryenhancementNew feature or requestNew feature or requestStatus: Open.#159 In FreeProving/free-compiler;Implement polymorphic let bindings
enhancementNew feature or requestNew feature or requestIRChanges of the intermediate representationChanges of the intermediate representationStatus: Open.#157 In FreeProving/free-compiler;Translated data types violate Coq's strict positivity restriction
bugSomething isn't workingSomething isn't workingCoqRelated to Coq back end or base libraryRelated to Coq back end or base libraryStatus: Open.#155 In FreeProving/free-compiler;Translate quick check properties to Agda
AgdaRelated to Agda back end or base libraryRelated to Agda back end or base libraryStatus: Open.#146 In FreeProving/free-compiler;