We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent bae336d commit 0339cd2Copy full SHA for 0339cd2
src/Lean/Compiler/LCNF/ToMono.lean
@@ -19,7 +19,7 @@ abbrev ToMonoM := StateRefT ToMonoM.State CompilerM
19
20
def Param.toMono (param : Param) : ToMonoM Param := do
21
if isTypeFormerType param.type then
22
- modify fun { typeParams, .. } => { typeParams := typeParams.insert param.fvarId }
+ modify fun s => { s with typeParams := s.typeParams.insert param.fvarId }
23
param.update (← toMonoType param.type)
24
25
def isTrivialConstructorApp? (declName : Name) (args : Array Arg) : ToMonoM (Option LetValue) := do
0 commit comments