Hoogle Search
Within LTS Haskell 24.52 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
-
Agda Agda.Syntax.Abstract No documentation available.
Primitive :: DefInfo -> QName -> Arg Type -> DeclarationAgda Agda.Syntax.Abstract primitive function
PrimitiveS :: DeclarationSpineAgda Agda.Syntax.Abstract No documentation available.
-
Agda Agda.Syntax.Abstract A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.
ProblemEq :: Pattern -> Term -> Dom Type -> ProblemEqAgda Agda.Syntax.Abstract No documentation available.
Proj :: ProjOrigin -> AmbiguousQName -> ExprAgda Agda.Syntax.Abstract Projection (overloaded).
ProjP :: PatInfo -> ProjOrigin -> AmbiguousQName -> Pattern' eAgda Agda.Syntax.Abstract Destructor pattern d.
module Agda.Syntax.Abstract.
Pattern Auxiliary functions to handle patterns in the abstract syntax. Generic and specific traversals.
-
Agda Agda.Syntax.Abstract.Pattern Converting a pattern to an expression. The Hiding context is remembered to create instance metas when translating absurd patterns in instance position.
module Agda.Syntax.Abstract.
PatternSynonyms Pattern synonym utilities: folding pattern synonym definitions for printing and merging pattern synonym definitions to handle overloaded pattern synonyms.