fixes for lean4#2973

leanprover-community · Nov 28, 2023 · ed2e76b · ed2e76b
1 parent d3a1d25
commit ed2e76b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Qq/Match.lean b/Qq/Match.lean
@@ -248,8 +248,8 @@ partial def isIrrefutablePattern : Term → Bool
 
 scoped elab "_comefrom" n:ident "do" b:doSeq " in " body:term : term <= expectedType => do
   let _ ← extractBind expectedType
-  (← elabTerm (← `(?m)).1.stripPos none).mvarId!.assign expectedType
-  elabTerm (← `(have $n:ident : ?m := (do $b:doSeq); $body)) expectedType
+  let ty ← exprToSyntax expectedType
+  elabTerm (← `(have $n:ident : $ty := (do $b:doSeq); $body)) expectedType
 
 scoped syntax "_comefrom" ident "do" doSeq : term
 macro_rules | `(assert! (_comefrom $n do $b); $body) => `(_comefrom $n do $b in $body)

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4-pr-releases:pr-release-2973
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.0.0
		leanprover/lean4-pr-releases:pr-release-2973