Abhishek Anand

jump to definition with dune

1

builds on https://github.com/cpitclaudel/company-coq/pull/257 this is unsafe in theory as there may just happen to be a _build/default directory without dune. we can add an explicit flag indicating dune somewhere, e.g....

It works fine for constructors of `Inductive`s

Is it possible for "jump to definition" to open the target in a new window. That way, one can interact with both files concurrently instead of retracting the old one.

jumping to lambda-bound or let-bound variables.

1

Would it be easy to implement jumping to local binders in a function? For example: ``` let x := ... in let y := .... in let z := x...

read-only access to gmail

4

I am concerned about the possibility of losing data due to possible bugs in gmvault. Most likely there aren't such bugs, but I only wish to use gmvault to backup...

inverse process

1

Any thoughts on how hard it would be to implement the inverse process: take a backup.xml and media directory and create an encrypted backup file that android would be able...

extraction mode: adding level to environment in unquote_universe

3

There seems to be a discrepancy in how `unquote_level` is instantiated in extraction mode and in template-coq (live-coq) mode. The extraction mode implementation is [here](https://github.com/MetaCoq/metacoq/blob/b6710f579cc2485927ba558ca2c5016d43486364/checker/src/term_quoter.ml#L344) and looks like: ```` let...

can we use this work as a C++ x86 emulation library?

3

We are looking for a trustworthy C++ library to emulate x86 instructions. Is it possible to use this work? Can the semantics in K be compiled to C/C++? if not,...

Is there a recommended reading order for the content in this library? The order in automatically the generated toc.html seems to be violating dependencies between modules. There used to be...