Idrall.Derive.Common

Reexports

Definitions

mkTy : Name -> TTImp -> ITy

  Named type.
  
  This is an alias for `MkTyp EmptyFC`.

Visibility: export

var : Name -> TTImp

  Creates a variable from the given name
  
  Names are best created using quotes: `{ AName },
  `{ In.Namespacs.Name }.
  
  Likewise, if the name is already known at the time of
  writing, use quotes for defining variables directly: `(AName)

Visibility: export

varStr : String -> TTImp

  Alias for `var . fromString`

Visibility: export

patClause : TTImp -> TTImp -> Clause

  A pattern clause consisting of the left-hand and
  right-hand side of the pattern arrow "=>".
  
  This is an alias for `PatClause EmptyFC`.

Visibility: export

stripNs : Name -> Name

  from idris2-lsp

Visibility: export

genReadableSym : String -> Elab Name

  from idris2-lsp

Visibility: export

primStr : String -> TTImp

  from idris2-lsp

Visibility: export

bindvar : Name -> TTImp

  from idris2-lsp

Visibility: export

implicit' : TTImp

  from idris2-lsp

Visibility: export

getArgs : TTImp -> Elab (List (Name, TTImp))

  moved from where clause

Visibility: export

Cons : Type

Visibility: public export

logCons : Cons -> Elab ()

Visibility: export

data IdrisType : Type

  Used with FromDhall interface, to dervice implementations
  for ADTs or Records

Totality: total
Visibility: public export
Constructors:

ADT : IdrisType

Record : IdrisType

record Options : Type

Totality: total
Visibility: public export
Constructor: 

MkOptions : (String -> String) -> Options

Projection: 

.fieldNameModifier : Options -> String -> String

  This function is used to adjust constructor argument names
  during encoding and decoding

.fieldNameModifier : Options -> String -> String

  This function is used to adjust constructor argument names
  during encoding and decoding

Visibility: public export

fieldNameModifier : Options -> String -> String

  This function is used to adjust constructor argument names
  during encoding and decoding

Visibility: public export

defaultOptions : Options

Visibility: export