Open lcrh opened 1 month ago
Perhaps the behavior changed here from previous versions of lean, but running the code from the book locally in vscode, I got the following error:
cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
Perhaps the behavior changed here from previous versions of lean, but running the code from the book locally in vscode, I got the following error: