Jared Roesch

icon company NVIDIA icon location Seattle, Washington icon location CTO @ OctoML, PMC @ Apache TVM, PhD @ UW. Previously Rustc, Lean & F* hacker.

Results 3 issues of Jared Roesch

expr patterns elaborate to very large terms

3 comment

`expr` patterns cause huge blow up for visually small patterns. An example from the smt2 interface: ```lean set_option eqn_compiler.max_steps 20000 meta def bad_elab : expr -> expr -> tactic unit...

P-low
E-hard
A-equation compiler
I-performance

[RFC] Implicit Quantification

9 comment

@leodemoura and I were talking today about adding support for implicit quantification. The goal of this feature is to remove needless repetitive typing. An example would be: ```lean def append...

P-low
E-hard
I-enhancement
A-elaborator
RFC

Not pragmatic enough

1 comment

I think you should check out some more pragmatic webframeworks like https://github.com/rails/rails. Is a Kleisli a type of sausage?