From 739ef7d166f4a49ef6c985bafbbd6150163558c3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Jan 2022 14:35:05 -0800 Subject: [PATCH] fix: annotate `let rec` declarations as `auxDecl` Reason: 1- Tactics such as `assumption` should ignore them. 2- We must annotate recursive applications with `mkRecAppWithSyntax`. --- src/Lean/Elab/LetRec.lean | 2 +- tests/lean/letRecMissingAnnotation.lean | 8 ++++++++ tests/lean/letRecMissingAnnotation.lean.expected.out | 5 +++++ 3 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 tests/lean/letRecMissingAnnotation.lean create mode 100644 tests/lean/letRecMissingAnnotation.lean.expected.out diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index fd621c1755..d3d6fcab0b 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -79,7 +79,7 @@ private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : A let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α := if h : i < views.size then let view := views.get ⟨i, h⟩ - withLocalDeclD view.shortDeclName view.type fun fvar => loop (i+1) (fvars.push fvar) + withLocalDecl view.shortDeclName BinderInfo.auxDecl view.type fun fvar => loop (i+1) (fvars.push fvar) else k fvars loop 0 #[] diff --git a/tests/lean/letRecMissingAnnotation.lean b/tests/lean/letRecMissingAnnotation.lean new file mode 100644 index 0000000000..b88696b5fb --- /dev/null +++ b/tests/lean/letRecMissingAnnotation.lean @@ -0,0 +1,8 @@ +def sum (as : Array Nat) : Nat := + let rec go (i : Nat) (s : Nat) : Nat := + if h : i < as.size then + go (i+2) (s + as.get ⟨i, h⟩) -- Error + else + s + go 0 0 +termination_by measure (fun ⟨a, i, _⟩ => a.size - i) diff --git a/tests/lean/letRecMissingAnnotation.lean.expected.out b/tests/lean/letRecMissingAnnotation.lean.expected.out new file mode 100644 index 0000000000..06403ceb7b --- /dev/null +++ b/tests/lean/letRecMissingAnnotation.lean.expected.out @@ -0,0 +1,5 @@ +letRecMissingAnnotation.lean:4:6-4:34: error: unsolved goals +as : Array Nat +i s : Nat +h : i < Array.size as +⊢ Array.size as - (i + 2) < Array.size as - i