max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add macro withoutExpectedType! <term>

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-27 11:08:58 -08:00
parent 09ed75f517
commit d212a5b671
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Notation.lean
View file

@ -107,6 +107,12 @@ macro_rules
| `({ $x : $type // $p }) => `(Subtype (fun ($x:ident : $type) => $p))
| `({ $x // $p }) => `(Subtype (fun ($x:ident : _) => $p))
/-
`withoutExpected! t` instructs Lean to elaborate `t` without an expected type.
Recall that terms such as `match ... with ...` and `⟨...⟩` will postpone elaboration until
expected type is known. So, `withoutExpected!` is not effective in this case. -/
macro "withoutExpectedType! " x:term : term => `(let aux := $x; aux)
namespace Lean.Parser.Tactic
syntax[intro] "intro " notFollowedBy("|") (colGt term:max)* : tactic