483f32edd8
This feature produced counterintuitive behavior and confused users. See discussion at #770. As pointed out by @tydeu, it is not too much work to write `Id.run <|` before the `do` when we want to use the `do` notation in pure code. closes #770
3 lines
83 B
Text
3 lines
83 B
Text
let_fun this := ();
|
|
this : Id Unit
|
|
commandPrefix.lean:3:0: error: expected command
|