Tej Chajed

`auto using` uses more powerful unification than `simple apply`

3

#### Version Coq 8.8+alpha (commit a2b02cb91) #### Operating system macOS #### Description of the problem `auto using pf` is more powerful than adding pf as a hint because it doesn't...

Test against multiple Coq versions

1

The only thing blocking this is that some examples demo coq master features, and these shouldn't be run on older versions. We can probably somehow set this up (without branches),...

Estimated time remaining does not take into account current iteration

1

Re-rendering the bar in the middle of an iteration updates the time since start, but the time remaining doesn't take into account the current iteration. Here's a [simple example video](https://asciinema.org/a/Ra8f84sP62Xu4Z9XJhhW2ADmU),...

For control flow and assignments, it would be conceptually clearer if we supported them by rewriting the AST to satisfy some invariant and then translating the result. For example, this...

Go has an (unusual) feature of infinite-precision computation of constant integer expressions, which are formally considered untyped in the language. Goose does not support untyped constants (which would be modeled...

Support calling pointer-receiver methods on struct fields

1

Right now we write code like ``` type foo struct { bar *Bar } func (f *foo) UseBar() { f.bar.DoSomething() } ``` This results in double dereferencing - once to...

Converting `len` to `uint32` via a type wrapper is mistranslated, dropping the type wrapper and using `slice.len` (which produces a `u64`). ```go type Uint32 uint32 func failing_testU32NewtypeLen() bool { s...

Rather than translate `const` declarations to global expressions, we should try to translate them to their value in `Z` and then use them as `#ConstName`. We would probably not bother...

In `for...range` loops over a map, we should support `break` similar to how ordinary `for` loops work. The concrete use case is code that finds an arbitrary element in a...