namespace http://cds.omdoc.org/urtheories❚
theory PL =
oftype # : 1❙
List # List 1❙
list # [ 1,… ]❙
Option # Option 1❙
some # some 1❙
none # none❙
Tuple # 1×…❙
tuple # ⟨ 1,… ⟩ ❙
proj # 1 . 2❙
Function # 1×… ⟶ 2❙
lambda # λ V1T,… . -2 prec 20❙
apply # 1@…❙
Nat # ℕ❙
plus # 1+…❙
times # 1*…❙
minus # 1 - 2❙
div # 1 / 2❙
less # 1 < 2❙
lesseq # 1 ≤ 2❙
greater # 1 > 2❙
greatereq # 1 ≥ 2❙
Boolean # ℬ
and # 1∧…❙
or # 1∨…❙
equal # 1 = 2❙
ifte # if ( 1 ) 2 else 3❙
match # 1 match 2|… prec 50❙
case # [ V2T,… ] 1 ⇝ 3 prec 5❙
❚