ATS Option Type Example

Run Settings
LanguageATS
Language Version
Run Command
#include "share/atspre_staload.hats" staload "libats/ML/SATS/basis.sats" (* // dependent type datatype option_t0ype_bool_type (a:t@ype+, bool) = | Some (a, true) of a | None (a, false) of () stadef option = option_t0ype_bool_type typedef Option (a:t0p) = [b:bool] option (a, b) *) (* // linear dependent type dataviewtype option_viewt0ype_bool_viewtype (a:viewt@ype+, bool) = | Some_vt (a, true) of a | None_vt (a, false) of () stadef option_vt = option_vt0ype_bool_vtype vtypedef Option_vt (a:vt0p) = [b:bool] option_vt (a, b) *) (* // naive datatype datatype option0_t0ype_type (a: t@ype+) = | Some0 of (a) | None0 of () stadef option0 = option0_t0ype_type *) implement main0 () = () where { val some = (Some 1) : option (int, true) val _ = case+ some of | Some x => println! ("Some: ", x) | None () => println! ("None") val somevt = Some_vt 2 : option_vt (int, true) val _ = case+ somevt of | ~Some_vt x => println! ("SomeVt: ", x) | ~None_vt () => println! ("NoneVt") val some0 = Some0 3 : option0 (int) val _ = case+ some0 of | Some0 x => println! ("Some0: ", x) | None0 () => println! ("None0") }
Editor Settings
Theme
Key bindings
Full width
Lines