Ruos

Failed to input the tactics step-by-step within a case block

3

First thanks for such excellent tools! I'm testing repl to see if I can enter the tactics one-by-one so that I can get state information within each step. When I...

current repl maybe cannot recognize mathcal letter?

7

When I was testing repl using the following example (it's actually the predefined theorem ```Metric.uniformity_basis_dist``` in mathlib4 ```Mathlib/Topology/MetricSpace/PseudoMetric.lean```): ```bash import Mathlib open Set Filter TopologicalSpace Bornology open scoped BigOperators ENNReal...