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

Generic Evidence

Defined in Wingman.Judgements.Theta

Associated Types

type Rep Evidence :: Type -> Type

Methods

from :: Evidence -> Rep Evidence x

to :: Rep Evidence x -> Evidence

type Rep Evidence

Defined in Wingman.Judgements.Theta

type Rep Evidence = D1 ('MetaData "Evidence" "Wingman.Judgements.Theta" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" 'False) (C1 ('MetaCons "EqualityOfTypes" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "HasInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PredType)))

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.