Core.Normalise.Quote

Definitions

data QVar : Type

Totality: total
Visibility: export

record QuoteOpts : Type

Totality: total
Visibility: public export
Constructor: 

MkQuoteOpts : Bool -> Bool -> Maybe Nat -> QuoteOpts

Projections:

.patterns : QuoteOpts -> Bool

.sizeLimit : QuoteOpts -> Maybe Nat

.topLevel : QuoteOpts -> Bool

.topLevel : QuoteOpts -> Bool

Visibility: public export

topLevel : QuoteOpts -> Bool

Visibility: public export

.patterns : QuoteOpts -> Bool

Visibility: public export

patterns : QuoteOpts -> Bool

Visibility: public export

.sizeLimit : QuoteOpts -> Maybe Nat

Visibility: public export

sizeLimit : QuoteOpts -> Maybe Nat

Visibility: public export

interface Quote : (List Name -> Type) -> Type

Parameters: tm
Methods:

quote : Ref Ctxt Defs => Defs -> Env Term vars -> tm vars -> Core (Term vars)

quoteLHS : Ref Ctxt Defs => Defs -> Env Term vars -> tm vars -> Core (Term vars)

quoteOpts : Ref Ctxt Defs => QuoteOpts -> Defs -> Env Term vars -> tm vars -> Core (Term vars)

quoteGen : Ref Ctxt Defs => Ref QVar Int -> QuoteOpts -> Defs -> Env Term vars -> tm vars -> Core (Term vars)

Implementations:

Quote NF

Quote Term

Quote Closure

quote : Quote tm => Ref Ctxt Defs => Defs -> Env Term vars -> tm vars -> Core (Term vars)

Visibility: public export

quoteLHS : Quote tm => Ref Ctxt Defs => Defs -> Env Term vars -> tm vars -> Core (Term vars)

Visibility: public export

quoteOpts : Quote tm => Ref Ctxt Defs => QuoteOpts -> Defs -> Env Term vars -> tm vars -> Core (Term vars)

Visibility: public export

quoteGen : Quote tm => Ref Ctxt Defs => Ref QVar Int -> QuoteOpts -> Defs -> Env Term vars -> tm vars -> Core (Term vars)

Visibility: public export

genName : Ref QVar Int => String -> Core Name

Visibility: export

quoteWithPi : Ref Ctxt Defs => Defs -> Env Term vars -> NF vars -> Core (Term vars)

Visibility: export