Output

Defines the structure of the training data, as well as how to translate internal Agda definition to this format.

Types

type Name = String

Name identifiers.

type DB = Int

DeBruijn indices.

type Head = Either Name DB

A head of a λ-application can either be a defined name in the global scope, or a DeBruijn index into the local context.

Generic constructions

pattern (:>) :: String -> a -> Pretty a infixr 4

data Pretty a

Bundle a thing with its "pretty" version.

NB: In JSON format, we follow a shallow encoding with "pretty" being an additional field and "thing" just inlined in the top-level record.

Constructors

Pretty

Fields

• pretty :: String
• thing :: a

Instances

Telescope ~> Telescope

Defined in Output

Methods

convert :: Telescope0 -> TCM Telescope

go :: Telescope0 -> TCM Telescope

FromJSON a => FromJSON (Pretty a)

Defined in Output

Methods

parseJSON :: Value -> Parser (Pretty a)

parseJSONList :: Value -> Parser [Pretty a]

ToJSON a => ToJSON (Pretty a)

Defined in Output

Methods

toJSON :: Pretty a -> Value

toEncoding :: Pretty a -> Encoding

toJSONList :: [Pretty a] -> Value

toEncodingList :: [Pretty a] -> Encoding

Generic (Pretty a)

Defined in Output

Associated Types

type Rep (Pretty a) :: Type -> Type

Methods

from :: Pretty a -> Rep (Pretty a) x

to :: Rep (Pretty a) x -> Pretty a

Show a => Show (Pretty a)

Defined in Output

Methods

showsPrec :: Int -> Pretty a -> ShowS

show :: Pretty a -> String

showList :: [Pretty a] -> ShowS

type Rep (Pretty a)

Defined in Output

type Rep (Pretty a) = D1 ('MetaData "Pretty" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) (C1 ('MetaCons "Pretty" 'PrefixI 'True) (S1 ('MetaSel ('Just "pretty") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "thing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

data Reduced a

Bundle a term with (several of) its normalised forms.

We do not repeat identical elements in subsequent evaluations (in the order simprednorm) and some fields may not be populated due to the evaluation taking to long and leading to a timeout (currently 2 seconds).

NB: Like Named, encoded in a shallow JSON.

Constructors

Reduced

Fields

• original :: a
• simplified :: Maybe a
• reduced :: Maybe a
• normalised :: Maybe a

Instances

Foldable Reduced

Defined in Output

Methods

fold :: Monoid m => Reduced m -> m

foldMap :: Monoid m => (a -> m) -> Reduced a -> m

foldMap' :: Monoid m => (a -> m) -> Reduced a -> m

foldr :: (a -> b -> b) -> b -> Reduced a -> b

foldr' :: (a -> b -> b) -> b -> Reduced a -> b

foldl :: (b -> a -> b) -> b -> Reduced a -> b

foldl' :: (b -> a -> b) -> b -> Reduced a -> b

foldr1 :: (a -> a -> a) -> Reduced a -> a

foldl1 :: (a -> a -> a) -> Reduced a -> a

toList :: Reduced a -> [a]

null :: Reduced a -> Bool

length :: Reduced a -> Int

elem :: Eq a => a -> Reduced a -> Bool

maximum :: Ord a => Reduced a -> a

minimum :: Ord a => Reduced a -> a

sum :: Num a => Reduced a -> a

product :: Num a => Reduced a -> a

Traversable Reduced

Defined in Output

Methods

traverse :: Applicative f => (a -> f b) -> Reduced a -> f (Reduced b)

sequenceA :: Applicative f => Reduced (f a) -> f (Reduced a)

mapM :: Monad m => (a -> m b) -> Reduced a -> m (Reduced b)

sequence :: Monad m => Reduced (m a) -> m (Reduced a)

Functor Reduced

Defined in Output

Methods

fmap :: (a -> b) -> Reduced a -> Reduced b

(<$) :: a -> Reduced b -> Reduced a

FromJSON a => FromJSON (Reduced a)

Defined in Output

Methods

parseJSON :: Value -> Parser (Reduced a)

parseJSONList :: Value -> Parser [Reduced a]

ToJSON a => ToJSON (Reduced a)

Defined in Output

Methods

toJSON :: Reduced a -> Value

toEncoding :: Reduced a -> Encoding

toJSONList :: [Reduced a] -> Value

toEncodingList :: [Reduced a] -> Encoding

Generic (Reduced a)

Defined in Output

Associated Types

type Rep (Reduced a) :: Type -> Type

Methods

from :: Reduced a -> Rep (Reduced a) x

to :: Rep (Reduced a) x -> Reduced a

Show a => Show (Reduced a)

Defined in Output

Methods

showsPrec :: Int -> Reduced a -> ShowS

show :: Reduced a -> String

showList :: [Reduced a] -> ShowS

type Rep (Reduced a)

Defined in Output

type Rep (Reduced a) = D1 ('MetaData "Reduced" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) (C1 ('MetaCons "Reduced" 'PrefixI 'True) ((S1 ('MetaSel ('Just "original") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "simplified") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe a))) :*: (S1 ('MetaSel ('Just "reduced") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe a)) :*: S1 ('MetaSel ('Just "normalised") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe a)))))

pattern (:~) :: Name -> a -> Named a infixr 4

data Named a

Bundle a thing with its name.

NB: Like Named and Reduced, encoded in a shallow JSON.

Constructors

Named

Fields

• name :: Name
• item :: a

Instances

Telescope ~> Telescope

Defined in Output

Methods

convert :: Telescope0 -> TCM Telescope

go :: Telescope0 -> TCM Telescope

FromJSON a => FromJSON (Named a)

Defined in Output

Methods

parseJSON :: Value -> Parser (Named a)

parseJSONList :: Value -> Parser [Named a]

ToJSON a => ToJSON (Named a)

Defined in Output

Methods

toJSON :: Named a -> Value

toEncoding :: Named a -> Encoding

toJSONList :: [Named a] -> Value

toEncodingList :: [Named a] -> Encoding

Generic (Named a)

Defined in Output

Associated Types

type Rep (Named a) :: Type -> Type

Methods

from :: Named a -> Rep (Named a) x

to :: Rep (Named a) x -> Named a

Show a => Show (Named a)

Defined in Output

Methods

showsPrec :: Int -> Named a -> ShowS

show :: Named a -> String

showList :: [Named a] -> ShowS

type Rep (Named a)

Defined in Output

type Rep (Named a) = D1 ('MetaData "Named" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) (C1 ('MetaCons "Named" 'PrefixI 'True) (S1 ('MetaSel ('Just "name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "item") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Concrete types (~ JSON schema)

type FileData = Named TrainData

Data for a file include the filename and its training data.

data TrainData

The training data for a module, divided into three parts.

Constructors

TrainData

Fields

• scopeGlobal :: [ScopeEntry]

  The global scope, giving the types and definitions of all import statements.

  NB: does not contain any holes for subterms.

• scopeLocal :: [ScopeEntry]

  The local scope, containing the types, definitions, and training data for each of this module's definitions.

• scopePrivate :: Maybe [ScopeEntry]

  The private scope, containing private definitions not exported to the public, as well as system-generated definitions stemming from where or with.

Instances

FromJSON TrainData

Defined in Output

Methods

parseJSON :: Value -> Parser TrainData

parseJSONList :: Value -> Parser [TrainData]

ToJSON TrainData

Defined in Output

Methods

toJSON :: TrainData -> Value

toEncoding :: TrainData -> Encoding

toJSONList :: [TrainData] -> Value

toEncodingList :: [TrainData] -> Encoding

Generic TrainData

Defined in Output

Associated Types

type Rep TrainData :: Type -> Type

Methods

from :: TrainData -> Rep TrainData x

to :: Rep TrainData x -> TrainData

type Rep TrainData

Defined in Output

type Rep TrainData = D1 ('MetaData "TrainData" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) (C1 ('MetaCons "TrainData" 'PrefixI 'True) (S1 ('MetaSel ('Just "scopeGlobal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ScopeEntry]) :*: (S1 ('MetaSel ('Just "scopeLocal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ScopeEntry]) :*: S1 ('MetaSel ('Just "scopePrivate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [ScopeEntry])))))

type ScopeEntry = Named ScopeEntry'

Every ScopeEntry' is named.

data ScopeEntry'

An entry in the scope: type, definitions, and holes.

Constructors

ScopeEntry

Fields

• _type :: Pretty (Reduced Type)

  The entry's type.

• definition :: Maybe (Pretty Definition)

  The actual body of this entry's definition.

• holes :: Maybe [Sample]

  Training data for each of the subterms in this entry's definition.

Instances

FromJSON ScopeEntry'

Defined in Output

Methods

parseJSON :: Value -> Parser ScopeEntry'

parseJSONList :: Value -> Parser [ScopeEntry']

ToJSON ScopeEntry'

Defined in Output

Methods

toJSON :: ScopeEntry' -> Value

toEncoding :: ScopeEntry' -> Encoding

toJSONList :: [ScopeEntry'] -> Value

toEncodingList :: [ScopeEntry'] -> Encoding

Generic ScopeEntry'

Defined in Output

Associated Types

type Rep ScopeEntry' :: Type -> Type

Methods

from :: ScopeEntry' -> Rep ScopeEntry' x

to :: Rep ScopeEntry' x -> ScopeEntry'

Show ScopeEntry'

Defined in Output

Methods

showsPrec :: Int -> ScopeEntry' -> ShowS

show :: ScopeEntry' -> String

showList :: [ScopeEntry'] -> ShowS

type Rep ScopeEntry'

Defined in Output

type Rep ScopeEntry' = D1 ('MetaData "ScopeEntry'" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) (C1 ('MetaCons "ScopeEntry" 'PrefixI 'True) (S1 ('MetaSel ('Just "_type") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pretty (Reduced Type))) :*: (S1 ('MetaSel ('Just "definition") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Pretty Definition))) :*: S1 ('MetaSel ('Just "holes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Sample])))))

data Sample

The training sample for each sub-hole.

Constructors

Sample

Fields

• ctx :: Pretty Telescope

  The current context, as a binding telescope.

• goal :: Pretty (Reduced Type)

  The current goal, i.e. type of the sub-term.

  NB: DeBruijn indices here refer to the ctx.

• term :: Pretty (Reduced Term)

  The term that successfully fills the current goal.

• premises :: [Name]

  Definitions used in this "proof", intended to be used for premise selection.

Instances

FromJSON Sample

Defined in Output

Methods

parseJSON :: Value -> Parser Sample

parseJSONList :: Value -> Parser [Sample]

ToJSON Sample

Defined in Output

Methods

toJSON :: Sample -> Value

toEncoding :: Sample -> Encoding

toJSONList :: [Sample] -> Value

toEncodingList :: [Sample] -> Encoding

Generic Sample

Defined in Output

Associated Types

type Rep Sample :: Type -> Type

Methods

from :: Sample -> Rep Sample x

to :: Rep Sample x -> Sample

Show Sample

Defined in Output

Methods

showsPrec :: Int -> Sample -> ShowS

show :: Sample -> String

showList :: [Sample] -> ShowS

type Rep Sample

Defined in Output

type Rep Sample = D1 ('MetaData "Sample" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) (C1 ('MetaCons "Sample" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ctx") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pretty Telescope)) :*: S1 ('MetaSel ('Just "goal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pretty (Reduced Type)))) :*: (S1 ('MetaSel ('Just "term") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pretty (Reduced Term))) :*: S1 ('MetaSel ('Just "premises") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))))

data Definition

Agda definitions: datatypes, records, functions, postulates and primitives.

Constructors

ADT

e.g. data ℕ : Set where zero : ℕ suc : ℕ → ℕ

Fields

• variants :: [Type]

Constructor

e.g. `(ℕ, 0) ~ zero` or `(ℕ, 1) ~ suc`

Fields

• reference :: Name
• variant :: Integer

Record

e.g. record X : Set where field x : ℕ y : ℕ

Fields

• telescope :: Telescope
• fields :: [Type]

Function

e.g. f [] = [] f (x ∷ xs) = x ∷ x ∷ xs

Fields

• clauses :: [Clause]

Postulate

e.g. `postulate pred : ℕ → ℕ`

Primitive

e.g. `primitive primShowNat : ℕ → String`

Instances

FromJSON Definition

Defined in Output

Methods

parseJSON :: Value -> Parser Definition

parseJSONList :: Value -> Parser [Definition]

ToJSON Definition

Defined in Output

Methods

toJSON :: Definition -> Value

toEncoding :: Definition -> Encoding

toJSONList :: [Definition] -> Value

toEncodingList :: [Definition] -> Encoding

Generic Definition

Defined in Output

Associated Types

type Rep Definition :: Type -> Type

Methods

from :: Definition -> Rep Definition x

to :: Rep Definition x -> Definition

Show Definition

Defined in Output

Methods

showsPrec :: Int -> Definition -> ShowS

show :: Definition -> String

showList :: [Definition] -> ShowS

Definition ~> Definition

Defined in Output

Methods

convert :: Definition0 -> TCM Definition

go :: Definition0 -> TCM Definition

Defn ~> Definition

Defined in Output

Methods

convert :: Defn -> TCM Definition

go :: Defn -> TCM Definition

type Rep Definition

Defined in Output

type Rep Definition = D1 ('MetaData "Definition" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) ((C1 ('MetaCons "ADT" 'PrefixI 'True) (S1 ('MetaSel ('Just "variants") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type])) :+: (C1 ('MetaCons "Constructor" 'PrefixI 'True) (S1 ('MetaSel ('Just "reference") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "variant") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "Record" 'PrefixI 'True) (S1 ('MetaSel ('Just "telescope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: S1 ('MetaSel ('Just "fields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type])))) :+: (C1 ('MetaCons "Function" 'PrefixI 'True) (S1 ('MetaSel ('Just "clauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])) :+: (C1 ('MetaCons "Postulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (U1 :: Type -> Type))))

data Clause

Function clauses.

Constructors

Clause

Fields

• _telescope :: Telescope

  the telescope induced by the clause's context and patterns

• patterns :: [Pattern]

  the actual patterns of this function clause

• body :: Maybe Term

  the right hand side of the clause (Nothing for absurd clauses)

Instances

FromJSON Clause

Defined in Output

Methods

parseJSON :: Value -> Parser Clause

parseJSONList :: Value -> Parser [Clause]

ToJSON Clause

Defined in Output

Methods

toJSON :: Clause -> Value

toEncoding :: Clause -> Encoding

toJSONList :: [Clause] -> Value

toEncodingList :: [Clause] -> Encoding

Generic Clause

Defined in Output

Associated Types

type Rep Clause :: Type -> Type

Methods

from :: Clause -> Rep Clause x

to :: Rep Clause x -> Clause

Show Clause

Defined in Output

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

Clause ~> Clause

Defined in Output

Methods

convert :: Clause0 -> TCM Clause

go :: Clause0 -> TCM Clause

type Rep Clause

Defined in Output

type Rep Clause = D1 ('MetaData "Clause" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) (S1 ('MetaSel ('Just "_telescope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Just "patterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern]) :*: S1 ('MetaSel ('Just "body") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Term)))))

type Telescope = [Named (Pretty Type)]

A telescope is a sequence of (named) types, a.k.a. bindings.

type Pattern = Term

We under-approximate patterns as terms, e.g. losing information about forced patterns.

type Type = Term

Types are the same as terms.

data Term

The AST of Agda terms.

Constructors

Pi Bool (Named Term) Term

e.g. ∀ {A : Set}. A → A

Lam (Named Term)

e.g. λ x. x

App Head [Term]

e.g. f x (x + x) or @0 (λ x. x)

Lit String

e.g. 42 or "something"

Sort String

e.g. Set

Level String

e.g. 0ℓ

UnsolvedMeta

i.e. {!!}

Instances

FromJSON Term

Defined in Output

Methods

parseJSON :: Value -> Parser Term

parseJSONList :: Value -> Parser [Term]

ToJSON Term

Defined in Output

Methods

toJSON :: Term -> Value

toEncoding :: Term -> Encoding

toJSONList :: [Term] -> Value

toEncodingList :: [Term] -> Encoding

Generic Term

Defined in Output

Associated Types

type Rep Term :: Type -> Type

Methods

from :: Term -> Rep Term x

to :: Rep Term x -> Term

Show Term

Defined in Output

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

DeBruijnPattern ~> Pattern

Defined in Output

Methods

convert :: DeBruijnPattern -> TCM Pattern

go :: DeBruijnPattern -> TCM Pattern

Elim ~> Term

Defined in Output

Methods

convert :: Elim -> TCM Term

go :: Elim -> TCM Term

Telescope ~> Telescope

Defined in Output

Methods

convert :: Telescope0 -> TCM Telescope

go :: Telescope0 -> TCM Telescope

Term ~> Term

Defined in Output

Methods

convert :: Term0 -> TCM Term

go :: Term0 -> TCM Term

Type ~> Type

Defined in Output

Methods

convert :: Type0 -> TCM Type

go :: Type0 -> TCM Type

type Rep Term

Defined in Output

type Rep Term = D1 ('MetaData "Term" "Output" "agda2train-0.0.3.0-inplace-agda2train-lib" 'False) ((C1 ('MetaCons "Pi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Named Term)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: (C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Named Term))) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Head) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term])))) :+: ((C1 ('MetaCons "Lit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "Sort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "Level" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "UnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type))))

Conversion from Agda's internal syntax

class a ~> b | a -> b where

Converting between two types a and b under Agda's typechecking monad.

NB: go is only used internally to de-clutter the recursive calls.

Minimal complete definition

go

Methods

convert :: a -> TCM b

go :: a -> TCM b

Instances

Clause ~> Clause

Defined in Output

Methods

convert :: Clause0 -> TCM Clause

go :: Clause0 -> TCM Clause

DeBruijnPattern ~> Pattern

Defined in Output

Methods

convert :: DeBruijnPattern -> TCM Pattern

go :: DeBruijnPattern -> TCM Pattern

Elim ~> Term

Defined in Output

Methods

convert :: Elim -> TCM Term

go :: Elim -> TCM Term

Telescope ~> Telescope

Defined in Output

Methods

convert :: Telescope0 -> TCM Telescope

go :: Telescope0 -> TCM Telescope

Term ~> Term

Defined in Output

Methods

convert :: Term0 -> TCM Term

go :: Term0 -> TCM Term

Type ~> Type

Defined in Output

Methods

convert :: Type0 -> TCM Type

go :: Type0 -> TCM Type

Definition ~> Definition

Defined in Output

Methods

convert :: Definition0 -> TCM Definition

go :: Definition0 -> TCM Definition

Defn ~> Definition

Defined in Output

Methods

convert :: Defn -> TCM Definition

go :: Defn -> TCM Definition

Utilities

pp :: Pretty a => a -> String

ppm :: (MonadPretty m, PrettyTCM a) => a -> m Doc

prender :: Doc -> String

pinterleave :: (Applicative m, Semigroup (m Doc)) => m Doc -> [m Doc] -> m Doc

pbindings :: (MonadPretty m, PrettyTCM a) => [(String, a)] -> [m Doc]

report :: MonadTCM m => VerboseLevel -> TCM Doc -> m ()

panic :: (Pretty a, Show a) => String -> a -> b

ppName :: QName -> String

unqualify :: QName -> String

(\/) :: (a -> Bool) -> (a -> Bool) -> a -> Bool

isNotCubical :: Clause -> Bool

jsonOpts :: Options

Configure JSON to omit empty (optional) fields and switch from camelCase to kebab-case.

Orphan instances

PrettyTCM Definition

Methods

prettyTCM :: MonadPretty m => Definition -> m Doc