Idris/ssg
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Disable smart constructor for now

Browse source
This commit is contained in:
Nathan McCarty 2025-02-19 05:00:28 -05:00
parent 2929bceaa1
commit 7f4bcf5f51
2 changed files with 16 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/SSG/HTML.idr
View file

@ -123,10 +123,10 @@ namespace Html
TagType' : (type : String) -> {auto prf : IsValidTag type} -> Type
TagType' type {prf} = TagType prf
||| Smart constructor for tags
public export
tag : (type : String) -> {auto prf : IsValidTag type} -> TagType prf
tag type {prf = (PVoid type)} = Void type
tag type {prf = (PRawText type)} = RawText type
tag type {prf = (PEscapableRawText type)} = RawText type
tag type {prf = (PNormal type)} = Normal type
-- ||| Smart constructor for tags
-- public export
-- tag : (type : String) -> {auto prf : IsValidTag type} -> TagType prf
-- tag type {prf = (PVoid type)} = Void type
-- tag type {prf = (PRawText type)} = RawText type
-- tag type {prf = (PEscapableRawText type)} = RawText type
-- tag type {prf = (PNormal type)} = Normal type