Leonardo de Moura
Leonardo de Moura
```lean import Lean syntax "foo " str : tactic open Lean Elab elab_rules : tactic | `(foo $x:str) => logInfo x.getString example : True := by foo "hello" -- Error...
We currently use the longest match parser combinator only when processing syntax categories. During the ICERM after-party hackton, users created fake "syntax category" to get the longest match behavior. BTW,...
@digama0 and I want to make sure tactics such as `Ring` can be invoked from `simp`.
This issue is a placeholder for collecting ideas and features for visualizing and filtering traces. @dselsam @Kha @Vtec234
Motivation: examples such as https://github.com/leanprover/lean4/blob/master/tests/lean/run/nestedInductiveRecType.lean In this example, `T` is a nested inductive type. So, in the current implementation, any recursive function is defined using well-founded recursion. However, functions defined...
Lean 3 has this feature. It has performance problems and limitations.
@Kha when `panic` is evaluated by the interpreter, the execution is interrupted as expected. However, all trace messages produced using `dbgTrace` are lost because the `#eval` command implementation redirects stdout...
Consider the following variants of a `cache` function ```lean import Lean set_option trace.compiler.ir.result true open Lean structure State where keys : Array Expr results : Array Expr abbrev M :=...