Wingman.Metaprogramming.ProofState

Documentation

renderSimplyDecorated

Arguments

:: Monoid out

=> (Text -> out)

Render plain Text

-> (ann -> out)

How to render an annotation

-> (ann -> out)

How to render the removed annotation

-> SimpleDocStream ann

-> out

data Ann

Constructors

Goal

Hypoth

Status

Instances

Bounded Ann

Defined in Wingman.Metaprogramming.ProofState

Methods

minBound :: Ann

maxBound :: Ann

Enum Ann

Defined in Wingman.Metaprogramming.ProofState

Methods

succ :: Ann -> Ann

pred :: Ann -> Ann

toEnum :: Int -> Ann

fromEnum :: Ann -> Int

enumFrom :: Ann -> [Ann]

enumFromThen :: Ann -> Ann -> [Ann]

enumFromTo :: Ann -> Ann -> [Ann]

enumFromThenTo :: Ann -> Ann -> Ann -> [Ann]

Eq Ann

Defined in Wingman.Metaprogramming.ProofState

Methods

(==) :: Ann -> Ann -> Bool

(/=) :: Ann -> Ann -> Bool

Ord Ann

Defined in Wingman.Metaprogramming.ProofState

Methods

compare :: Ann -> Ann -> Ordering

(<) :: Ann -> Ann -> Bool

(<=) :: Ann -> Ann -> Bool

(>) :: Ann -> Ann -> Bool

(>=) :: Ann -> Ann -> Bool

max :: Ann -> Ann -> Ann

min :: Ann -> Ann -> Ann

Show Ann

Defined in Wingman.Metaprogramming.ProofState

Methods

showsPrec :: Int -> Ann -> ShowS

show :: Ann -> String

showList :: [Ann] -> ShowS

forceMarkdownNewlines :: String -> String

layout :: Bool -> Doc Ann -> String

renderAnn :: Bool -> Ann -> Text

renderUnann :: Bool -> Ann -> Text

proofState :: RunTacticResults -> Doc Ann

prettySubgoal :: Judgement -> Doc Ann

prettyHypothesis :: Hypothesis CType -> Doc Ann

prettyHyInfo :: HyInfo CType -> Doc Ann

prettyType :: CType -> Doc Ann

countFinished :: Doc Ann -> Doc Ann -> Int -> Doc Ann

count :: Doc Ann -> Int -> Doc Ann

textSpaces :: Int -> Text