72a6169 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Display of lifted types

Run errReverse, so that we get the pre-normalised type synonyms. This is mostly to avoid displaying IO', but perhaps there is ultimately a better way of deciding how to display things which arise from type synonyms.

commit72a6169cacc0ee88c19d227aa2ef72052beff22a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 17 Jun 2016, 16:02 (10 years ago) parent55230b7

1 file changed+8−4

compare with master

unifiedsplit

src/Idris/Interactive.hs+8−4

src/Idris/Interactive.hs+8−4

@@ -20,6 +20,7 @@ import Idris.CaseSplit

2020import Idris.AbsSyntax

2121import Idris.ElabDecls

2222import Idris.Error

23+import Idris.ErrReverse

2324import Idris.Delaborate

2425import Idris.Output

2526import Idris.IdeMode hiding (IdeModeCommand(..))

@@ -333,11 +334,14 @@ makeLemma fn updatefile l n

333334 let isProv = checkProv tyline (show n)

334335

335336 ctxt <- getContext

336− (fname, mty) <- case lookupTyName n ctxt of

337− [t] -> return t

338− [] -> ierror (NoSuchVariable n)

339− ns -> ierror (CantResolveAlts (map fst ns))

337+ (fname, mty_full) <- case lookupTyName n ctxt of

338+ [t] -> return t

339+ [] -> ierror (NoSuchVariable n)

340+ ns -> ierror (CantResolveAlts (map fst ns))

341+

340342 i <- getIState

343+ let mty = errReverse i mty_full

344+

341345 margs <- case lookup fname (idris_metavars i) of

342346 Just (_, arity, _, _, _) -> return arity

343347 _ -> return (-1)