@@ -1405,7 +1405,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14051405 -- Build the LHS as an "Infer", and pull out its type and
14061406 -- pattern bindings
14071407 i <- getIState
1408− let lhs = addImplPat i lhs_in
1408+ let lhs = addImplPat i (stripLinear i lhs_in)
14091409 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
14101410 ((lhs', dlhs, []), _) <-
14111411 tclift $ elaborate ctxt (MN 0 "patLHS") infP []