on master help sign in
Don't normalise types
047be9eEdwin Brady
src/Idris/ElabDecls.hs+1−1
@@ -58,7 +58,7 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in
58 (cty, _) <- recheckC fc [] tyT
58 (cty, _) <- recheckC fc [] tyT
59 addStatics n cty ty'
59 addStatics n cty ty'
60 logLvl 2 $ "---> " ++ show cty
60 logLvl 2 $ "---> " ++ show cty
61− let nty = normalise ctxt [] cty
61+ let nty = cty -- normalise ctxt [] cty
62 ds <- checkDef fc [(n, nty)]
62 ds <- checkDef fc [(n, nty)]
63 addIBC (IBCDef n)
63 addIBC (IBCDef n)
64 addDeferred ds
64 addDeferred ds