refinedToJsonDef : Name -> (p : ParamTypeInfo) -> RefinedInfo p -> Decl- Totality: total
Visibility: export RefinedToJSONVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel) Generate declarations and implementations for
`FromJSON` for a given refinement type.
Totality: total
Visibility: exportRefinedToJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)- Totality: total
Visibility: export refineFromJSON : FromJSON a => String -> (a -> Maybe b) -> Parser JSON b- Totality: total
Visibility: public export refinedFromJsonDef : Name -> Name -> Name -> Decl- Totality: total
Visibility: export RefinedFromJSONVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel) Generate declarations and implementations for
`FromJSON` for a given refinement type.
Totality: total
Visibility: exportRefinedFromJSON : List Name -> ParamTypeInfo -> Res (List TopLevel)- Totality: total
Visibility: export RefinedJSON : List Name -> ParamTypeInfo -> Res (List TopLevel) Generate declarations and implementations for
`FromJSON` and `ToJSON` for a given refinement type.
Totality: total
Visibility: export