5602ea7 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+1−3

@@ -31,9 +31,7 @@ data Command = Theorem Name Raw

31 | Tac (Elab ())

32

33data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

34−

34+ deriving Show

35−instance Pretty aux => Pretty (ElabState aux) where

36− pretty (ES (pState, aux) str _) = text "test"

37

35

38type Elab' aux a = StateT (ElabState aux) TC a

36type Elab' aux a = StateT (ElabState aux) TC a

39type Elab a = Elab' () a

37type Elab a = Elab' () a

src/Core/ProofShell.hs+1−1

@@ -52,7 +52,7 @@ processCommand (Tac e) state

52 (pterm ps')

53 (ptype ps')

54 (context ps') }, resp)

55− err -> (state, show . render . pretty $ err)

55+ err -> (state, show err)

56 | otherwise = (state, "No proof in progress")

57

58runShell :: ShellState -> InputT IO ShellState

src/Core/TT.hs+1−1

@@ -1,4 +1,4 @@

1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, FlexibleInstances #-}

1+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

2

3module Core.TT where

4