Permalink
Browse files

Add toString function for Rat values (no proof)

  • Loading branch information...
myreen committed Oct 10, 2017
1 parent c882c6b commit 135b0887b898b29455b3d43398927112eef38278
Showing with 8 additions and 0 deletions.
  1. +8 −0 basis/mlratProgScript.sml
@@ -339,6 +339,14 @@ val pair_div_v_thm =
|> DISCH_ALL |> REWRITE_RULE [pair_div_side_def] |> UNDISCH_ALL
|> add_user_proved_v_thm;
val toString_def = Define `
toString (i:int,n:num) =
if n = 1 then mlint$toString i else
concat [mlint$toString i ; implode"/" ; mlint$toString (& n)]`
val _ = (next_ml_names := ["toString"]);
val v = translate toString_def;
val EqualityType_REAL_TYPE = store_thm("EqualityType_REAL_TYPE",
``EqualityType REAL_TYPE``,
rw [EqualityType_def]

0 comments on commit 135b088

Please sign in to comment.