view lib/basis.lig @ 103:8921f0344193

Command-line compiler goes the whole nine yards
author Adam Chlipala <adamc@hcoop.net>
date Thu, 10 Jul 2008 14:14:23 -0400
parents 94afff1ff7f6
children b1e5398a7f30
line wrap: on
line source
type int
type float
type string


con tag :: {Unit} -> {Unit} -> Type


con xml :: {Unit} -> Type
val cdata : ctx ::: {Unit} -> string -> xml ctx
val tag : outer ::: {Unit} -> inner ::: {Unit}
        -> tag outer inner
        -> xml inner
        -> xml outer
val join : shared :: {Unit}
        -> ctx1 ::: {Unit} -> ctx1 ~ shared
        -> ctx2 ::: {Unit} -> ctx2 ~ shared
        -> xml (shared ++ ctx1) -> xml (shared ++ ctx2) -> xml shared


val head : tag [Html] [Head]
val title : tag [Head] []

val body : tag [Html] [Body]
val p : tag [Body] [Body]
val b : tag [Body] [Body]
val i : tag [Body] [Body]