Antal Spector-Zabusky

Uniform treatment of translation, axiomatization, and skipping

10

@sweirich in [a comment] on commit 4cd6596, about `unaxiomatize definition`: > How about something a little more general, so that we can have "skip everything except for this" too. >...

Mutual recursion does not work with differing type arguments

3

Consider the following painfully contrived Haskell code: ```haskell module BadMut where data Nat = Z | S Nat sink :: Nat -> a -> a sink Z x = x...

Deal with `Default` instance generation

2

As we saw in #100 (preserving record names), our story for tracking `Default` instances isn't great and needs some manual skipping. As I understand it, #100 introduces too many `Default`...

Some edits should be local (renames), some should not be local (renames for other reasons). This should be expanded on.

Split out the examples from the source code

3

There's a lot going on in this repository: 1. The `hs-to-coq` conversion tool itself 2. An abandoned GHC plugin that enables converting between structurally isomorphic types 3. The converted parts...

`merlin-locate` fails in the presence of certain type errors

1

We've had some bugs about `merlin-locate` (jump to definition/implementation) reported internally, which are all about it not succeeding when there's some sort of type error present in the code. We're...

Right now, `quil-rs` defines the `WaveformTemplate` trait, but doesn't actually make any internal use of it. We should provide integration between it and the rest of `quil-rs`; at a minimum,...