TTImp.WithClause

Definitions

getMatch : Ref MD Metadata => Ref Ctxt Defs => Bool -> RawImp -> RawImp -> Core (List (Name, RawImp))

Visibility: export

getNewLHS : Ref Ctxt Defs => Ref MD Metadata => FC -> Nat -> NestedNames vars -> Name -> List (Maybe (PiInfo RawImp, Name)) -> RawImp -> RawImp -> Core RawImp

Visibility: export

withRHS : Ref Ctxt Defs => Ref MD Metadata => FC -> Nat -> Name -> List (Maybe (PiInfo RawImp, Name)) -> RawImp -> RawImp -> Core RawImp

Visibility: export