Wingman.Judgements.Theta

Documentation

data Evidence

Something we've learned about the type environment.

Instances

Show Evidence

Defined in Wingman.Judgements.Theta

Methods

showsPrec :: Int -> Evidence -> ShowS

show :: Evidence -> String

showList :: [Evidence] -> ShowS

getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]

Compute all the Evidence implicitly bound at the given SrcSpan.

mkEvidence :: PredType -> [Evidence]

Given a PredType, pull an Evidence out of it.

evidenceToSubst :: Evidence -> TacticState -> TacticState

Update our knowledge of which types are equal.

evidenceToHypothesis :: Evidence -> Hypothesis CType

Get all of the methods that are in scope from this piece of Evidence.

evidenceToThetaType :: [Evidence] -> Set CType

Build a set of PredTypes from the evidence.