antalsz/hs-to-coq

Issues

• Derived Ord instances do a weird substitution

  #176 opened 4 years ago by Lysxia
  4

• Skip types from a skipped module

  #166 opened 4 years ago by Lysxia
  0

• Pattern synonyms

  #164 opened 4 years ago by Lysxia
  1

• Code duplication in mutually recursive functions

  #162 opened 4 years ago by trommler
  0

• Rename type doesn't affect signature when used with "in"

  #156 opened 5 years ago by ericgiovannini
  1

• Use `Equations` instead of `Program Fixpoint` for termination

  #138 opened 5 years ago by joscoh
  4

• Qualify modules under base

  #158 opened 5 years ago by Lysxia
  1

• Don't include Makefile generated by Coq

  #157 opened 5 years ago by Lysxia
  0

• Rename our provided modules from `GHC.…` to `HsToCoq.…` or similar

  #155 opened 5 years ago by antalsz
  0

• Universe polymorphism edits

  #151 opened 5 years ago by lastland
  8

• GHC flags taken into account too late

  #152 opened 5 years ago by nomeata
  0

• What is the meaning of GHC.Err.patternFailure?

  #150 opened 5 years ago by christinaburge
  3

• Coqc doesn't recognise !! operator

  #149 opened 5 years ago by christinaburge
  0

• Cannot find a physical path bound to logical path matching suffix GHC.

  #144 opened 5 years ago by christinaburge
  20

• Generate Rewrite Tactics for Unfolding Definitions

  #140 opened 5 years ago by euisuny
  2

• hs-to-coq goes into a seeming infinite loop with memory explosion

  #112 opened 5 years ago by jwiegley
  3

• CI breaks because of the wc example

  #147 opened 5 years ago by lastland
  0

• Edit files without trailing line breaks parser

  #143 opened 5 years ago by euisuny
  0

• Redefine does not work on default type class methods

  #142 opened 5 years ago by lastland
  0

• The float_let tactic breaks with Coq 8.10.2

  #139 opened 5 years ago by lastland
  0

• `rename value` does not respect `rename module`

  #137 opened 5 years ago by lastland
  0

• Add/redefine (axiomatized) instances for redefined types

  #136 opened 6 years ago by sweirich
  2

• Cannot axiomatize and rename the same module

  #129 opened 6 years ago by sweirich
  2

• Automatically delete redundant cases/equations

  #135 opened 6 years ago by antalsz
  5

• skip constructor

  #130 opened 6 years ago by sweirich
  2

• skip constructor: collectAnnArgsTicks

  #132 opened 6 years ago by sweirich
  3

• skip constructor: expr_fvs

  #133 opened 6 years ago by sweirich
  2

• skip constructor: eqExpr

  #134 opened 6 years ago by sweirich
  1

• skip constructor: substUnfolding

  #131 opened 6 years ago by sweirich
  0

• Prove debug assertions?

  #125 opened 6 years ago by antalsz
  1

• don't remove asserts from GHC

  #114 opened 6 years ago by sweirich
  1

• Create a way to axiomatize or skip top-level pattern bindings

  #104 opened 6 years ago by antalsz
  1

• Termination edits for "Default" functions

  #128 opened 6 years ago by sweirich
  0

• "Safe" axiomatization

  #127 opened 6 years ago by sweirich
  0

• `add let type` edit

  #110 opened 6 years ago by antalsz
  3

• Translating ADTs with constructors containing type variables

  #120 opened 6 years ago by lastland
  0

• Error building base.

  #123 opened 6 years ago by DavidFHCh
  2

• Better `rewrite` engine

  #124 opened 6 years ago by antalsz
  2

• How tied to your particular needs is your Coq AST/pretty-printer?

  #119 opened 6 years ago by Ptival
  3

• coq-haskell ?

  #122 opened 6 years ago by spitters
  3

• Add type definitions edit, including axioms

  #117 opened 6 years ago by sweirich
  0

• hs-to-coq doesn't accept minimal implementation of Ord in terms of (<=)

  #116 opened 6 years ago by emarzion
  1

• Rewrite for types

  #115 opened 6 years ago by antalsz
  0

• add skip field edit

  #113 opened 6 years ago by sweirich
  0

• Parameterized `order` edits

  #111 opened 6 years ago by antalsz
  4

• Pull out uniform fixpoint arguments

  #109 opened 6 years ago by antalsz
  2

• Custom class info

  #108 opened 6 years ago by antalsz
  0

• Kind polymorphism introduces spurious variables

  #107 opened 6 years ago by antalsz
  0

• Garbage-collect code base

  #106 opened 6 years ago by antalsz
  0

• Uniform treatment of translation, axiomatization, and skipping

  #105 opened 6 years ago by antalsz
  10