Safe Haskell	None
Language	Haskell2010

F

Documentation

type TyName = Name Ty Source #

type TmName = Name Tm Source #

data Ty Source #

Constructors

TyVar TyName
TyInt
Arr Ty Ty
All (Bind TyName Ty)
TyProd [Ty]

Instances

Show Ty Source #
Methods showsPrec :: Int -> Ty -> ShowS # show :: Ty -> String # showList :: [Ty] -> ShowS #
Rep Ty Source #
Methods rep :: R Ty #
Alpha Ty Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Ty -> Ty # fv' :: Collection f => AlphaCtx -> Ty -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Ty -> (Ty -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Ty -> m (Ty, Perm AnyName) # aeq' :: AlphaCtx -> Ty -> Ty -> Bool # acompare' :: AlphaCtx -> Ty -> Ty -> Ordering # close :: Alpha b => AlphaCtx -> b -> Ty -> Ty # open :: Alpha b => AlphaCtx -> b -> Ty -> Ty # isPat :: Ty -> Maybe [AnyName] # isTerm :: Ty -> Bool # isEmbed :: Ty -> Bool # nthpatrec :: Ty -> NthCont # findpatrec :: Ty -> AnyName -> FindResult #
Display Ty Source #
Methods display :: Ty -> DM Doc Source #
(Sat (ctx0 TyName), Sat (ctx0 Ty), Sat (ctx0 (Bind TyName Ty)), Sat (ctx0 [Ty])) => Rep1 ctx0 Ty Source #
Methods rep1 :: R1 ctx0 Ty #
Subst Tm Ty Source #
Methods isvar :: Ty -> Maybe (SubstName Ty Tm) # isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Tm) # subst :: Name Tm -> Tm -> Ty -> Ty # substs :: [(Name Tm, Tm)] -> Ty -> Ty # substPat :: AlphaCtx -> Tm -> Ty -> Ty # substPats :: Proxy * Tm -> AlphaCtx -> [Dyn] -> Ty -> Ty #
Subst Ty Prim Source #
Methods isvar :: Prim -> Maybe (SubstName Prim Ty) # isCoerceVar :: Prim -> Maybe (SubstCoerce Prim Ty) # subst :: Name Ty -> Ty -> Prim -> Prim # substs :: [(Name Ty, Ty)] -> Prim -> Prim # substPat :: AlphaCtx -> Ty -> Prim -> Prim # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Prim -> Prim #
Subst Ty Tm Source #
Methods isvar :: Tm -> Maybe (SubstName Tm Ty) # isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Ty) # subst :: Name Ty -> Ty -> Tm -> Tm # substs :: [(Name Ty, Ty)] -> Tm -> Tm # substPat :: AlphaCtx -> Ty -> Tm -> Tm # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Tm -> Tm #
Subst Ty Ty Source #
Methods isvar :: Ty -> Maybe (SubstName Ty Ty) # isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Ty) # subst :: Name Ty -> Ty -> Ty -> Ty # substs :: [(Name Ty, Ty)] -> Ty -> Ty # substPat :: AlphaCtx -> Ty -> Ty -> Ty # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Ty -> Ty #

data Tm Source #

Constructors

TmInt Int
TmVar TmName
Fix (Bind (TmName, TmName, Embed (Ty, Ty)) Tm)
App Tm Tm
TmProd [Tm]
TmPrj Tm Int
TmPrim Tm Prim Tm
TmIf0 Tm Tm Tm
TLam (Bind TyName Tm)
TApp Tm Ty
Ann Tm Ty

Instances

Show Tm Source #
Methods showsPrec :: Int -> Tm -> ShowS # show :: Tm -> String # showList :: [Tm] -> ShowS #
Rep Tm Source #
Methods rep :: R Tm #
Alpha Tm Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Tm -> Tm # fv' :: Collection f => AlphaCtx -> Tm -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Tm -> (Tm -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Tm -> m (Tm, Perm AnyName) # aeq' :: AlphaCtx -> Tm -> Tm -> Bool # acompare' :: AlphaCtx -> Tm -> Tm -> Ordering # close :: Alpha b => AlphaCtx -> b -> Tm -> Tm # open :: Alpha b => AlphaCtx -> b -> Tm -> Tm # isPat :: Tm -> Maybe [AnyName] # isTerm :: Tm -> Bool # isEmbed :: Tm -> Bool # nthpatrec :: Tm -> NthCont # findpatrec :: Tm -> AnyName -> FindResult #
Display Tm Source #
Methods display :: Tm -> DM Doc Source #
(Sat (ctx0 Int), Sat (ctx0 TmName), Sat (ctx0 (Bind (TmName, TmName, Embed (Ty, Ty)) Tm)), Sat (ctx0 Tm), Sat (ctx0 [Tm]), Sat (ctx0 Prim), Sat (ctx0 (Bind TyName Tm)), Sat (ctx0 Ty)) => Rep1 ctx0 Tm Source #
Methods rep1 :: R1 ctx0 Tm #
Subst Tm Prim Source #
Methods isvar :: Prim -> Maybe (SubstName Prim Tm) # isCoerceVar :: Prim -> Maybe (SubstCoerce Prim Tm) # subst :: Name Tm -> Tm -> Prim -> Prim # substs :: [(Name Tm, Tm)] -> Prim -> Prim # substPat :: AlphaCtx -> Tm -> Prim -> Prim # substPats :: Proxy * Tm -> AlphaCtx -> [Dyn] -> Prim -> Prim #
Subst Tm Tm Source #
Methods isvar :: Tm -> Maybe (SubstName Tm Tm) # isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Tm) # subst :: Name Tm -> Tm -> Tm -> Tm # substs :: [(Name Tm, Tm)] -> Tm -> Tm # substPat :: AlphaCtx -> Tm -> Tm -> Tm # substPats :: Proxy * Tm -> AlphaCtx -> [Dyn] -> Tm -> Tm #
Subst Tm Ty Source #
Methods isvar :: Ty -> Maybe (SubstName Ty Tm) # isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Tm) # subst :: Name Tm -> Tm -> Ty -> Ty # substs :: [(Name Tm, Tm)] -> Ty -> Ty # substPat :: AlphaCtx -> Tm -> Ty -> Ty # substPats :: Proxy * Tm -> AlphaCtx -> [Dyn] -> Ty -> Ty #
Subst Ty Tm Source #
Methods isvar :: Tm -> Maybe (SubstName Tm Ty) # isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Ty) # subst :: Name Ty -> Ty -> Tm -> Tm # substs :: [(Name Ty, Ty)] -> Tm -> Tm # substPat :: AlphaCtx -> Ty -> Tm -> Tm # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Tm -> Tm #

rTm1 :: forall ctx. ctx Int -> ctx TmName -> ctx (Bind (TmName, TmName, Embed (Ty, Ty)) Tm) -> (ctx Tm, ctx Tm) -> ctx [Tm] -> (ctx Tm, ctx Int) -> (ctx Tm, ctx Prim, ctx Tm) -> (ctx Tm, ctx Tm, ctx Tm) -> ctx (Bind TyName Tm) -> (ctx Tm, ctx Ty) -> (ctx Tm, ctx Ty) -> R1 ctx Tm Source #