fix: ComputedFields.lean
`all` fields was not being set correctly. TODO: check `all` fields in the kernel.
This commit is contained in:
parent
ea3235c551
commit
bd21583d4b
1 changed files with 4 additions and 2 deletions
|
|
@ -108,10 +108,12 @@ def overrideCasesOn : M Unit := do
|
|||
forallTelescope (← inferType minor) fun args _ => do
|
||||
mkLambdaFVars ((if ← isScalarField ctor then #[] else compFieldVars) ++ args)
|
||||
(← mkUnsafeCastTo constMotive (mkAppN minor args)))
|
||||
let nameOverride := mkCasesOnName name ++ `_override
|
||||
addDecl <| .defnDecl { casesOn with
|
||||
name := mkCasesOnName name ++ `_override
|
||||
name := nameOverride
|
||||
all := [nameOverride]
|
||||
value
|
||||
hints := .opaque
|
||||
hints := .opaque
|
||||
safety := .unsafe
|
||||
}
|
||||
setInlineAttribute (mkCasesOnName name ++ `_override)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue