% mathematical symbols by Anthony Phan.
% file: mathadrv.mf (driver file for matha serie)
% last modification: April 29, 2002.

mode_setup;

math_setup;

% Activate to allow characters with undefined code.
% (for proof mode compilation)
% let iff=always_iff;

% BINARY OPERATORS, RELATIONS

input mathasym;

% RELATIONS

% MISCELLANEOUS

negation_sign        :=hex"20";% we're not making any text font
dominated            :=hex"21";
dominating           :=hex"22";
hash_sign            :=hex"23";

not_sign             :=hex"7F";

%negation_sign        :=hex"26";
%reverse_negation_sign:=hex"27";

vdash_sign :=hex"24";
dashv_sign :=hex"25";
vdash_not  :=hex"26";
dashv_not  :=hex"27";
vDash_sign :=hex"28";
Dashv_sign :=hex"29";
vDash_not  :=hex"2A";
Dashv_not  :=hex"2B";
Vdash_sign :=hex"2C";
dashV_sign :=hex"2D";
Vdash_not  :=hex"2E";
dashV_not  :=hex"2F";
% hex"30"...hex"35", numerals...

degree_sign    :=hex"30";
prime_sign     :=hex"31";
second_sign    :=hex"32";
third_sign     :=hex"33";
fourth_sign    :=hex"34";

ligtable prime_sign  : prime_sign =: second_sign;
ligtable second_sign : prime_sign =: third_sign;
ligtable third_sign  : prime_sign =: fourth_sign;

musical_flat_sign:=hex"35";
musical_natural_sign:=hex"36";
musical_sharp_sign:=hex"37";

% mathfine.mf

Infinity        :=hex"38";
proportionnal_to:=hex"39";
dagger          :=hex"3A";
double_dagger   :=hex"3B";

% upper_asterisk:=hex"3A"; lower_asterisk:=hex"3B";
% triple_asterisk:=hex"3C";
% colon_sign:=hex"5B";

Dominated :=hex"CE";
Dominating:=hex"CF";

% LETTER LIKE SYMBOLS

% mathltlk.mf

for_all         :=hex"40";
complement      :=hex"41";
partial         :=hex"42";
partial_slash   :=hex"43";
there_exists    :=hex"44";
there_not_exists:=hex"45";
F_inverse       :=hex"46";
G_inverse       :=hex"47";
empty_set       :=hex"48";
diameter_sign   :=hex"49";
top_sign        :=hex"4A";
bot_sign        :=hex"4B";
not_top_sign    :=hex"4C";
not_bot_sign    :=hex"4D";
wedge_curly     :=hex"4E";
vee_curly       :=hex"4F";
%%%%%%%% Q_inverse:=hex"4A";
%%%%%%%% Bourbaki_Z:=hex"4F";

belong_to            :=hex"50";
not_belong_to        :=hex"52";
var_not_belong_to    :=hex"54";
belong_to_bar        :=hex"56";
rev_belong_to        :=hex"51";
not_rev_belong_to    :=hex"53";
var_not_rev_belong_to:=hex"55";
rev_belong_to_bar    :=hex"57";

cap_sign  :=hex"58";
cup_sign  :=hex"59";
cup_plus  :=hex"5A";
sqcap_sign:=hex"5B";
sqcup_sign:=hex"5C";
sqcup_plus:=hex"5D";
wedge_sign:=hex"5E";
vee_sign  :=hex"5F";

% DELIMITERS

paren_left     :=hex"70";
paren_right    :=hex"71";
bracket_left   :=hex"72";
bracket_right  :=hex"73";
brace_left     :=hex"74";
brace_right    :=hex"75";
bbbracket_left :=hex"76";
bbbracket_right:=hex"77";
angle_left     :=hex"78";
angle_right    :=hex"79";
backslash      :=hex"7A";
slash          :=hex"7B";
vert_sign      :=hex"7C";
vvert_sign     :=hex"7D";
vvvert_sign    :=hex"7E";

% TRIANGLES AS RELATIONS

triangle_left       :=hex"98"; triangle_right       :=hex"99";
not_triangle_left   :=hex"9A"; not_triangle_right   :=hex"9B";
triangle_left_eq    :=hex"9C"; triangle_right_eq    :=hex"9D";
not_triangle_left_eq:=hex"9E"; not_triangle_right_eq:=hex"9F";

% ARROWS and HARPOONS

arrow_left          :=hex"D0";
arrow_right         :=hex"D1";
arrow_up            :=hex"D2";
arrow_down          :=hex"D3";
arrow_northwest     :=hex"D4";
arrow_northeast     :=hex"D5";
arrow_southwest     :=hex"D6";
arrow_southeast     :=hex"D7";
arrow_left_right    :=hex"D8";
arrow_up_down       :=hex"D9";
arrow_left_not      :=hex"DA";
arrow_right_not     :=hex"DB";
arrow_left_right_not:=hex"DC";

relbar_char   :=hex"DD";
maps_to_char  :=hex"DE";
maps_from_char:=hex"DF";

harpoon_left_up     :=hex"E0";
harpoon_right_up    :=hex"E1";
harpoon_left_down   :=hex"E2";
harpoon_right_down  :=hex"E3";
harpoon_up_left     :=hex"E4";
harpoon_down_left   :=hex"E5";
harpoon_up_right    :=hex"E6";
harpoon_down_right  :=hex"E7";
harpoons_left_right :=hex"E8";
harpoons_right_left :=hex"E9";
harpoons_up_down    :=hex"EA";
harpoons_down_up    :=hex"EB";

double_arrow_left          :=hex"F0";
double_arrow_right         :=hex"F1";
double_arrow_up            :=hex"F2";
double_arrow_down          :=hex"F3";
double_arrow_left_right    :=hex"F4";
double_arrow_up_down       :=hex"F5";
double_arrow_left_not      :=hex"F6";
double_arrow_right_not     :=hex"F7";
double_arrow_left_right_not:=hex"F8";
Relbar_char                :=hex"F9";
Maps_to_char               :=hex"FA";
Maps_from_char             :=hex"FB";

% let the show begin :

input mathltlk;
input mathfine;
input mathsmsy;
input mathsymb;
input matharrw;
input mathbdel;

main_name_string:="subset";
t:=hex"80";
forsuffixes $=,_not,_eq,_not_eq,_eq_not,
  _eq_varnot,_eqq,_not_eqq,_eqq_not,_eqq_varnot,
  _double,_double_not:
  main_name_with($):=t; t:=t+2; endfor;
input mathsubs;

main_name_string:="supset";
t:=hex"81";
forsuffixes $=,_not,_eq,_not_eq,_eq_not,
  _eq_varnot,_eqq,_not_eqq,_eqq_not,_eqq_varnot,
  _double,_double_not:
  main_name_with($):=t; t:=t+2; endfor;
input mathsubs;

main_name_string:="less";
t:=hex"A0";
forsuffixes $=,_not,_slant,_not_slant,
  _eq,_not_eq,_eq_not,%_eqvarnot,
  _eqq,_not_eqq,_eqq_not,_eqq_varnot,
  _upperslant,_not_upperslant,
  _opposite,_eq_opposite,_eqq_opposite,
  _sim,_not_sim,_sim_not,_approx,_not_approx,_approx_not,_dot:
  main_name_with($):=t; t:=t+2; endfor;
input mathineq;

main_name_string:="greater";
t:=hex"A1";
forsuffixes $=,_not,_slant,_not_slant,
  _eq,_not_eq,_eq_not,%_eq_varnot,
  _eqq,_not_eqq,_eqq_not,_eqq_varnot,
  _upperslant,_not_upperslant,
  _opposite,_eq_opposite,_eqq_opposite,
  _sim,_not_sim,_sim_not,_approx,_not_approx,_approx_not,_dot:
  main_name_with($):=t; t:=t+2; endfor;
input mathineq;

main_name_string:="mcircle";% ``m'' stands for medium.
t:=hex"60";
forsuffixes $=_plus,_minus,_times,_division,
  _dot,_circle,_asterisk,_co_asterisk,
  _left,_right,_top,_bot,
  _sign,_slash,_backslash,_triangle_up:
  main_name_with($):=t; t:=t+1; endfor;
input mathmbcb;

% see also:
% _peace_and_love,_ying_yang,
% _truc,_curt,_full_circle,_five_star,_six_star,
% _triangle_down,_triangle_left,_triangle_right,
% _top_dot_minus,_bot_dot_minus,_horiz,_vert,_cross,_across,
% _wedge,_vee,
% _black_left,_black_right,_black_top,_black_bot,
% _black_northwest,_black_northeast,_black_southwest,_black_southeast:


% parameters for TFM files.

font_slant=0;
font_x_height=x_height#;
%font_normal_stretch=3u#;
%font_normal_shrink=2u#;
font_quad=18u#+4letter_fit#;
font_extra_space=2u#;
font_normal_space=6u#+2letter_fit#;

end.