| syntax (name := mycheck) "#check" sepBy(term, ",") : command | |
| open Lean | |
| macro_rules (kind := mycheck) | |
| | `(#check $es,*) => | |
| let cmds := es.getElems.map $ fun e => mkNode `Lean.Parser.Command.check #[mkAtom "#check", e] | |
| pure $ mkNullNode cmds | |
| /-- info: Bool.true : Bool -/ | |
| #guard_msgs in | |
| #check true | |
| /-- | |
| info: Bool.true : Bool | |
| --- | |
| info: Bool.true : Bool | |
| -/ | |
| #guard_msgs in | |
| #check true, true | |
| /-- | |
| info: Bool.true : Bool | |
| --- | |
| info: 1 : Nat | |
| --- | |
| info: 3 : Nat | |
| --- | |
| info: fun x => x + 1 : Nat → Nat | |
| -/ | |
| #guard_msgs in | |
| #check true, 1, 3, fun (x : Nat) => x + 1 |