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

fix: missing mkCIdents in Lean.Elab.Deriving.Util

Browse source
This commit is contained in:
Sebastian Ullrich 2023-07-24 15:50:38 +02:00 • committed by Leonardo de Moura
parent 8ffb389f3f
commit b15d6d41b8
2 changed files with 24 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Elab/Deriving/Util.lean
View file

@ -27,7 +27,7 @@ def mkInductArgNames (indVal : InductiveVal) : TermElabM (Array Name) := do
/-- Return the inductive declaration's type applied to the arguments in `argNames`. -/
def mkInductiveApp (indVal : InductiveVal) (argNames : Array Name) : TermElabM Term :=
let f := mkIdent indVal.name
let f := mkCIdent indVal.name
let args := argNames.map mkIdent
`(@$f $args*)
@ -54,7 +54,7 @@ def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames :
let c ← mkAppM className #[x]
if (← isTypeCorrect c) then
let argName := argNames[i]!
let binder : Syntax ← `(instBinderF| [ $(mkIdent className):ident $(mkIdent argName):ident ])
let binder : Syntax ← `(instBinderF| [ $(mkCIdent className):ident $(mkIdent argName):ident ])
binders := binders.push binder
catch _ =>
pure ()
@ -94,7 +94,7 @@ def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array
let binders ← mkImplicitBinders currIndices
let argNamesNew := argNames[:numParams] ++ currIndices
let indType ← mkInductiveApp indVal argNamesNew
let type ← `($(mkIdent className) $indType)
let type ← `($(mkCIdent className) $indType)
let val ← `(⟨$(mkIdent auxFunName)⟩)
let instName ← mkFreshUserName `localinst
let letDecl ← `(Parser.Term.letDecl| $(mkIdent instName):ident $binders:implicitBinder* : $type := $val)
@ -116,8 +116,10 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
let binders ← mkImplicitBinders argNames
let binders := binders ++ (← mkInstImplicitBinders className indVal argNames)
let indType ← mkInductiveApp indVal argNames
let type ← `($(mkIdent className) $indType)
let val ← if useAnonCtor then `(⟨$(mkIdent auxFunName)⟩) else pure <| mkIdent auxFunName
let type ← `($(mkCIdent className) $indType)
let mut val := mkIdent auxFunName
if useAnonCtor then
val ← `(⟨$val⟩)
let instCmd ← `(instance $binders:implicitBinder* : $type := $val)
instances := instances.push instCmd
return instances

17
tests/lean/run/2344.lean Normal file
View file

@ -0,0 +1,17 @@
namespace Value
inductive Primitive where
| Bool (b : Bool)
| Int (i : Int)
| String (s : String)
deriving instance DecidableEq for Primitive -- Works
inductive Value where
| Primitive (p : Primitive)
deriving instance DecidableEq for Primitive -- (no longer) fails
deriving instance DecidableEq for _root_.Value.Primitive -- (no longer) fails
deriving instance Repr for Primitive
deriving instance Repr for _root_.Value.Primitive