Derive.Lens.Options

Definitions

record LensOptions : Type

Totality: total
Visibility: public export
Constructor: 

MkLensOptions : (String -> String) -> (String -> String) -> (String -> String) -> LensOptions

Projections:

.constructorName : LensOptions -> String -> String

.dataTypeName : LensOptions -> String -> String

.fieldName : LensOptions -> String -> String

.fieldName : LensOptions -> String -> String

Totality: total
Visibility: public export

fieldName : LensOptions -> String -> String

Totality: total
Visibility: public export

.constructorName : LensOptions -> String -> String

Totality: total
Visibility: public export

constructorName : LensOptions -> String -> String

Totality: total
Visibility: public export

.dataTypeName : LensOptions -> String -> String

Totality: total
Visibility: public export

dataTypeName : LensOptions -> String -> String

Totality: total
Visibility: public export

toLowerHead : String -> String

Totality: total
Visibility: export

defaultOptions : LensOptions

Totality: total
Visibility: export