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

fix: missing ensureHasType

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-18 09:12:31 -08:00
parent ba93e9b895
commit c7fcb2c5a7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Elab/StructInst.lean
View file

@ -529,8 +529,8 @@ private partial def elabStruct : Struct → Option Expr → TermElabM (Expr × S
pure (e, type, field::fields)
};
match field.val with
| FieldVal.term stx => do val ← elabTerm stx (some d); continue val field
| FieldVal.nested s => do (val, sNew) ← elabStruct s (some d); continue val { val := FieldVal.nested sNew, .. field }
| FieldVal.term stx => do val ← elabTerm stx (some d); val ← ensureHasType stx d val; continue val field
| FieldVal.nested s => do (val, sNew) ← elabStruct s (some d); val ← ensureHasType s.ref d val; continue val { val := FieldVal.nested sNew, .. field }
| FieldVal.default => do val ← mkFreshExprMVar field.ref (some d); continue (markDefaultMissing val) field
| _ => throwFailedToElabField field.ref fieldName s.structName ("unexpected constructor type" ++ indentExpr type)
| _ => throwError field.ref "unexpected unexpanded structure field")