Check result of elaboration at the REPL properly
commit17387750f29042220324a17459399fec61739f87
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateThu 29 Nov 2012, 00:12 (14 years ago)
parent3187e59
src/Idris/ElabDecls.hs+1
@@ -455,6 +455,7 @@ elabVal info aspat tm_in
455455 (elaborate ctxt (MN 0 "val") infP []
456456 (build i info aspat (MN 0 "val") (infTerm tm)))
457457 logLvl 3 ("Value: " ++ show tm')
458+ recheckC (FC "(input)" 0) [] tm'
458459 let vtm = getInferTerm tm'
459460 logLvl 2 (show vtm)
460461 recheckC (FC "(input)" 0) [] vtm