Documentation

exprPlate :: Applicative f => (Expr -> f Expr) -> Expr -> f Expr Source

_App :: Prism' Expr (Name, [Expr]) Source

_Let :: Prism' Expr (Pattern, Expr, Expr) Source

_If :: Prism' Expr (Expr, Expr, Expr) Source

_Match :: Prism' Expr ([Expr], [(Pattern, Expr)]) Source

_Conn :: Prism' Expr (Conn, Expr, Expr) Source

_Not :: Prism' Expr Expr Source

_Quant :: Prism' Expr (Quant, [(Name, Type)], [[Expr]], Expr) Source

_Field :: Prism' Expr (Name, Expr) Source

_Record :: Prism' Expr [(Name, Expr)] Source

_RecordUpdate :: Prism' Expr (Expr, [(Name, Expr)]) Source

_Cast :: Prism' Expr (Expr, Type) Source

_Labeled :: Prism' Expr (Name, Expr) Source

_And :: Prism' Conn () Source

_AsymAnd :: Prism' Conn () Source

_Or :: Prism' Conn () Source

_AsymOr :: Prism' Conn () Source

_Implies :: Prism' Conn () Source

_Iff :: Prism' Conn () Source

_Goal :: Prism' Decl (Name, Expr) Source

_Use :: Prism' Decl (Maybe ImpExp, Name, Maybe Name) Source

_Axiom :: Prism' Decl (Name, Expr) Source

_Lemma :: Prism' Decl (Name, Expr) Source

_Type :: Prism' Decl (Name, [Text], [(Name, [Text])]) Source

_TypeDef :: Prism' Decl (Name, [Text], [(Name, [Text])], TypeDef) Source

_Predicate :: Prism' Decl (Name, [Text], [Type]) Source

_PredicateDef :: Prism' Decl (Name, [Text], [(Maybe Name, Type)], Expr) Source

_Function :: Prism' Decl (Name, [Text], [Type], Type) Source

_FunctionDef :: Prism' Decl (Name, [Text], [(Maybe Name, Type)], Type, Expr) Source

_Import :: Prism' ImpExp () Source

_Export :: Prism' ImpExp () Source

_Integer :: Prism' Literal Integer Source

_Real :: Prism' Literal Text Source

_Bool :: Prism' Literal Bool Source

_PWild :: Prism' Pattern () Source

_PVar :: Prism' Pattern Name Source

_PCon :: Prism' Pattern (Name, [Pattern]) Source

_Forall :: Prism' Quant () Source

_Exists :: Prism' Quant () Source

theoryName :: Lens' Theory Name Source

theoryDecls :: Lens' Theory [Decl] Source

tyCaseAltName :: Lens' TyCaseAlt Name Source

tyCaseAltLabels :: Lens' TyCaseAlt [Text] Source

tyCaseAltTyParams :: Lens' TyCaseAlt [(Maybe Name, Type)] Source

_TyCon :: Prism' Type (Name, [Type]) Source

_TyVar :: Prism' Type Name Source

_Tuple :: Prism' Type [Type] Source

_TyRecord :: Prism' TypeDef [(Name, Type)] Source

_Ty :: Prism' TypeDef Type Source

_TyCase :: Prism' TypeDef [TyCaseAlt] Source