TTImp.Interactive.CaseSplit

Definitions

data ClauseUpdate : Type

Totality: total
Visibility: public export
Constructors:

Valid : RawImp -> List (Name, RawImp) -> ClauseUpdate

Impossible : RawImp -> ClauseUpdate

Invalid : ClauseUpdate

Hint: 

Show ClauseUpdate

data SplitError : Type

Totality: total
Visibility: public export
Constructors:

NoValidSplit : SplitError

CantSplitThis : Name -> String -> SplitError

CantFindLHS : SplitError

Hint: 

Show SplitError

data SplitResult : Type -> Type

Totality: total
Visibility: public export
Constructors:

SplitFail : SplitError -> SplitResult a

OK : a -> SplitResult a

Hint: 

Show a => Show (SplitResult a)

explicitlyBound : Defs -> ClosedNF -> Core (List Name)

Visibility: export

getEnvArgNames : Ref Ctxt Defs => Defs -> Nat -> ClosedNF -> Core (List String)

Visibility: export

getSplitsLHS : Ref Ctxt Defs => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => FC -> Nat -> ClosedTerm -> Name -> Core (SplitResult (List ClauseUpdate))

Visibility: export

getSplits : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => (NonEmptyFC -> ClosedTerm -> Bool) -> Name -> Core (SplitResult (List ClauseUpdate))

Visibility: export