Amos Robinson
Amos Robinson
Name overlap: `Error` as variant constructor and type constructor as in following example: ``` type R e a = < Error e | Ok a > type Error = xxx...
See https://github.com/amosr/limp-cbc/issues/6
This adds a `[@@no_inline_let]` annotation so that the norm tactic doesn't always unfold local lets. I had to update the rlimit in some places. Some of these were necessary to...
Hi, I just noticed that `preprocess_with` does not deal well with records. A record constructor `{ x = 0; y = 1}` generates a term like `__dummy__ 0 1`. If...
I came across an error when defining a tactic that uses a local recursive definition as well as repeat. The `--codegen krml` extraction fails with a "this should not happen"...
I ran into an issue where normalization got stuck evaluating a mostly-concrete term. After talking on Slack, @nikswamy was surprised that normalization-by-evaluation stops under pattern matches. @mtzguido also suggested `zeta_full`...
Trying to apply normalize-by-evaluation to a reified effect fails with `Failure("NBE ill-typed application: Meta …")`. I was hoping to use the effects to build up a complex datastructure (an AST),...
Hello, I found an issue where `reflect_arith` in CoqIde wasn't undoing properly. So if I applied `reflect_arith`, went back one step, I would still have the `eval` stuff, then I...
Icicle[1] is a streaming query language that uses a type system to ensure that queries can be executed in a single-pass over the input stream with no buffering, and that...
Icicle is a streaming query language for machine-learning feature generation. Icicle must currently be run in batch mode over the day or the week's data set. We would like to...