Emulating type ascriptions

Stream: lean4

[Eric Wieser]

Why does this copy-paste implementation of ( :) not behave the same way as ( :)?

import Lean

open Lean Elab Term

/-- A version of `(t :)` that does not process `·`s in `t`.

This should be preferred inside macros. -/
syntax (name := withNoExpectedType) "with_no_expected_type(" term ")" : term

@[term_elab withNoExpectedType, inherit_doc withNoExpectedType]
def elabWithNoExpectedType : TermElab
  -- copied from `elabTypeAscription`
  | `(with_no_expected_type($e)), expectedType? => do
    let e ← withSynthesize (postpone := .no) <| elabTerm e none
    ensureHasType expectedType? e
  | _, _ => throwUnsupportedSyntax

-- works
/--
error: unsolved goals
p : Prop
h : p
⊢ ¬p
-/
#guard_msgs in
example {p : Prop} {h : p} : ∀ {h : True}, 0 = 0 := by
  refine (absurd h ?_ :)

-- extra `True` hypothesis
/--
error: unsolved goals
p : Prop
h : p
h✝ : True
⊢ ¬p
-/
#guard_msgs in
example {p : Prop} {h : p} : ∀ {h : True}, 0 = 0 := by
  refine with_no_expected_type(absurd h ?_)

[Aaron Liu]

lambda autoinsertion

[Aaron Liu]

I'll investigate

[Aaron Liu]

The difference seems to be in private def useImplicitLambda

[Eric Wieser]

Or rather, in blockImplicitLambda; thanks for finding that!

[Eric Wieser]

So I guess the answer is to add no_implicit_lambda

[Eric Wieser]

I can't seem to make this work:

import Lean

open Lean Elab Term Parser

/-- A set of parentheses which does not process `·` -/
@[term_parser]
def withoutCDot := leading_parser
  "without_cdot(" >> (withoutPosition (withoutForbidden (termParser >> optional (" :" >> optional (ppSpace >> termParser))))) >> ")"

@[term_elab withoutCDot, inherit_doc withoutCDot]
def elabWithoutCDot : TermElab
  -- copied from `elabTypeAscription`, with extra mkNoImplicitLambdaAnnotation
  | `(without_cdot($e : $type)), _ => do
    let type ← withSynthesize (postpone := .yes) <| elabType type
    let type := mkNoImplicitLambdaAnnotation type
    let e ← elabTerm e type
    ensureHasType type e
  | `(without_cdot($e :)), expectedType? => do
    let e ← withSynthesize (postpone := .no) <| elabTerm e none
    ensureHasType (mkNoImplicitLambdaAnnotation <$> expectedType?) e
  | `(without_cdot($e)), expectedType? => do
    elabTerm e expectedType?
  | _, _ => throwUnsupportedSyntax

-- extra `True` hypothesis
/--
error: unsolved goals
p : Prop
h : p
⊢ ¬p
-/
#guard_msgs in
example {p : Prop} {h : p} : ∀ {h : True}, 0 = 0 := by
  -- works only if you backspace `without_cdot`
  refine without_cdot(absurd h ?_ :)

[Eric Wieser]

Ah, I made this work with an intermediate elaborator, PR to mathlib incoming :)

[Eric Wieser]

#23257