@@ -455,6 +455,7 @@ elabVal info aspat tm_in
455 (elaborate ctxt (MN 0 "val") infP []
455 (elaborate ctxt (MN 0 "val") infP []
456 (build i info aspat (MN 0 "val") (infTerm tm)))
456 (build i info aspat (MN 0 "val") (infTerm tm)))
457 logLvl 3 ("Value: " ++ show tm')
457 logLvl 3 ("Value: " ++ show tm')
458+ recheckC (FC "(input)" 0) [] tm'
458 let vtm = getInferTerm tm'
459 let vtm = getInferTerm tm'
459 logLvl 2 (show vtm)
460 logLvl 2 (show vtm)
460 recheckC (FC "(input)" 0) [] vtm
461 recheckC (FC "(input)" 0) [] vtm