a6e3f09 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Special case for displaying Type : Type 1

...because people get the wrong impression about universes otherwise!

commita6e3f0985dcaf2527976d9222f520f25e581d1d0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 21 Jul 2013, 22:52 (13 years ago) parent0b25ad1

1 file changed+10−7

unifiedsplit

src/Idris/REPL.hs+10−7

@@ -323,13 +323,16 @@ process fn (Check (PRef _ n))

323323 showImp imp (delabTy ist n)) ts

324324 iResult ""

325325 [] -> iFail $ "No such variable " ++ show n

326−process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

327− ctxt <- getContext

328− ist <- getIState

329− imp <- impShow

330− let ty' = normaliseC ctxt [] ty

331− iResult (showImp imp (delab ist tm) ++ " : " ++

332− showImp imp (delab ist ty))

326+process fn (Check t)

327+ = do (tm, ty) <- elabVal toplevel False t

328+ ctxt <- getContext

329+ ist <- getIState

330+ imp <- impShow

331+ let ty' = normaliseC ctxt [] ty

332+ case tm of

333+ TType _ -> iResult ("Type : Type 1")

334+ _ -> iResult (showImp imp (delab ist tm) ++ " : " ++

335+ showImp imp (delab ist ty))

333336

334337process fn (DocStr n) = do i <- getIState

335338 case lookupCtxtName n (idris_docstrings i) of