feat: simplify decide! and nativeDecide! macros

src/Lean/Elab/BuiltinNotation.lean

@@ -156,25 +156,20 @@ fun stx _ => do
     let eq ← mkEq e val
     mkExpectedTypeHint r eq
 
-private def getPropToDecide (arg : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
-if arg.isOfKind `Lean.Parser.Term.hole then
-  tryPostponeIfNoneOrMVar expectedType?
-  match expectedType? with
-  | none => throwError "invalid macro, expected type is not available"
-  | some expectedType =>
-    synthesizeSyntheticMVars
-    let expectedType ← instantiateMVars expectedType
-    if expectedType.hasFVar || expectedType.hasMVar then
-      throwError! "expected type must not contain free or meta variables{indentExpr expectedType}"
-    pure expectedType
-else
-  let prop := mkSort levelZero
-  elabClosedTerm arg prop
+private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
+tryPostponeIfNoneOrMVar expectedType?
+match expectedType? with
+| none => throwError "invalid macro, expected type is not available"
+| some expectedType =>
+  synthesizeSyntheticMVars
+  let expectedType ← instantiateMVars expectedType
+  if expectedType.hasFVar || expectedType.hasMVar then
+    throwError! "expected type must not contain free or meta variables{indentExpr expectedType}"
+  pure expectedType
 
 @[builtinTermElab «nativeDecide»] def elabNativeDecide : TermElab :=
 fun stx expectedType? => do
-  let arg  := stx[1]
-  let p ← getPropToDecide arg expectedType?
+  let p ← getPropToDecide expectedType?
   let d ← mkAppM `Decidable.decide #[p]
   let auxDeclName ← mkNativeReflAuxDecl (Lean.mkConst `Bool) d
   let rflPrf ← mkEqRefl (toExpr true)
@@ -183,8 +178,7 @@ fun stx expectedType? => do
 
 @[builtinTermElab Lean.Parser.Term.decide] def elabDecide : TermElab :=
 fun stx expectedType? => do
-  let arg  := stx[1]
-  let p ← getPropToDecide arg expectedType?
+  let p ← getPropToDecide expectedType?
   let d ← mkAppM `Decidable.decide #[p]
   let d ← instantiateMVars d
   let s := d.appArg! -- get instance from `d`

src/Lean/Parser/Term.lean

@@ -170,8 +170,8 @@ def letRecDecls      := sepBy1 (group (optional «attributes» >> letDecl)) ", "
     parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >> optSemicolon termParser
 
 @[builtinTermParser] def nativeRefl   := parser! "nativeRefl! " >> termParser maxPrec
-@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec
-@[builtinTermParser] def decide       := parser! "decide! " >> termParser maxPrec
+@[builtinTermParser] def nativeDecide := parser! "nativeDecide!"
+@[builtinTermParser] def decide       := parser! "decide!"
 
 @[builtinTermParser] def typeOf             := parser! "typeOf! " >> termParser maxPrec
 @[builtinTermParser] def ensureTypeOf       := parser! "ensureTypeOf! " >> termParser maxPrec >> strLit >> termParser

tests/lean/run/doNotation3.lean

@@ -11,7 +11,7 @@ let rec loop : (i : Nat) → i ≤ as.size → β → m β
   | 0,   h, b => b
   | i+1, h, b => do
     have h' : i < as.size          from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
-    have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (decide! (0 < 1))
+    have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (decide! : (0:Nat) < 1)
     have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
     let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
     loop i (Nat.leOfLt h') b
@@ -28,7 +28,7 @@ let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
   | 0,   h => return b
   | i+1, h =>
     have h' : i < as.size          from Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
-    have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (decide! (0 < 1))
+    have as.size - 1 < as.size     from Nat.subLt (zeroLtOfLt h') (decide! : (0:Nat) < 1)
     have as.size - 1 - i < as.size from Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
     let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
     loop i (Nat.leOfLt h') b

tests/lean/run/reduce1.lean

@@ -20,23 +20,23 @@ theorem tst4 : 10000000000000000 < 200000000000000000000 :=
 ofDecideEqTrue (nativeRefl! (decide (10000000000000000 < 200000000000000000000)))
 
 theorem tst5 : 10000000000000000 < 200000000000000000000 :=
-nativeDecide! (10000000000000000 < 200000000000000000000)
+nativeDecide!
 
 theorem tst6 : 10000000000000000 < 200000000000000000000 :=
-let h₁ := nativeDecide! (10000000000000000 < 10000000000000010);
-let h₂ := nativeDecide! (10000000000000010 < 200000000000000000000);
+let h₁ := (nativeDecide! : (10000000000000000:Nat) < 10000000000000010)
+let h₂ := (nativeDecide! : (10000000000000010:Nat) < 200000000000000000000)
 Nat.ltTrans h₁ h₂
 
 theorem tst7 : 10000000000000000 < 200000000000000000000 :=
-decide! (10000000000000000 < 200000000000000000000)
+decide!
 
 theorem tst8 : 10000000000000000 < 200000000000000000000 :=
-let h₁ := decide! (10000000000000000 < 10000000000000010);
-let h₂ := decide! (10000000000000010 < 200000000000000000000);
+let h₁ := (decide! : (10000000000000000:Nat) < 10000000000000010)
+let h₂ := (decide! : (10000000000000010:Nat) < 200000000000000000000)
 Nat.ltTrans h₁ h₂
 
 theorem tst9 : 10000000000000000 < 200000000000000000000 :=
-decide! _
+decide!
 
 theorem tst10 : 10000000000000000 < 200000000000000000000 :=
-nativeDecide! _
+nativeDecide!

tests/lean/run/reduce3.lean

@@ -32,15 +32,15 @@ theorem tst8 : "hello" ++ "world" = "helloworld" :=
 rfl
 
 theorem tst9 : "abc" ≠ "cde" :=
-decide! _
+decide!
 
 theorem tst10 : "helloWorld" ≠ "helloworld" :=
-decide! _
+decide!
 
 theorem tst11 : "helloWorld" = "helloWorld" :=
-decide! _
+decide!
 
 theorem tst12 : 'a' ≠ 'c' :=
-decide! _
+decide!
 
 #check tst10