3770b3dcb8
This PR fixed typos: ``` pip install codespell --upgrade codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex '[A-Z][a-z]*' codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex "\b[a-z']*" ```
11 lines
245 B
Text
11 lines
245 B
Text
import Std.Tactic.Do
|
|
|
|
open Std.Do
|
|
|
|
set_option mvcgen.warning false
|
|
|
|
-- The following used to print the Syntax object representing `abc`
|
|
|
|
/-- error: Could not resolve spec theorem `abc` -/
|
|
#guard_msgs (error) in
|
|
example : True := by mvcgen [abc]
|