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

fix: disable auto implicits in structure field default values

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-18 23:17:36 +02:00 • committed by Leonardo de Moura
parent 2d28a9dd94
commit 987785242f
3 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Structure.lean
View file

@ -500,7 +500,7 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
Term.synthesizeSyntheticMVarsNoPostponing
-- TODO: add forbidden predicate using `shortDeclName` from `view`
let params ← Term.addAutoBoundImplicits params
let value ← Term.elabTerm valStx none
let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
let value ← mkLambdaFVars params value
return (none, value)
| some typeStx =>
@ -512,7 +512,7 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
let type ← mkForallFVars params type
return (type, none)
| some valStx =>
let value ← Term.elabTermEnsuringType valStx type
let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
Term.synthesizeSyntheticMVarsNoPostponing
let type ← mkForallFVars params type
let value ← mkLambdaFVars params value

7
tests/lean/autoImplicitForbidden.lean
View file

@ -21,3 +21,10 @@ mutual
inductive Ex2 : Type
end
structure Bar :=
(x : Na)
(y : Nat := foobar) -- Error at `foobar`
#print Bar.mk

2
tests/lean/autoImplicitForbidden.lean.expected.out
View file

@ -3,3 +3,5 @@ autoImplicitForbidden.lean:6:10-6:11: error: unknown identifier 'h'
autoImplicitForbidden.lean:13:24-13:27: error: unknown identifier 'Bla'
autoImplicitForbidden.lean:16:21-16:24: error: unknown identifier 'Foo'
autoImplicitForbidden.lean:20:18-20:21: error: unknown identifier 'Ex2'
autoImplicitForbidden.lean:28:14-28:20: error: unknown identifier 'foobar'
constructor Bar.mk.{u_1} : ({Na : Sort u_1} → Na) → Nat → Bar