(* Author: MakariusExample theory involving Unicode characters (UTF-8 encoding) -- both formal and informal ones. \<open>A Hebrew theory\<close> theory Hebrewimports Mainbegin text \<open> \<^bold>\<open>Warning:\<close> Bidirectional Unicode text may confuse display in browsers, editors, etc.! \<close> \<open>The Hebrew Alef-Bet (א-ב).\<close> datatype alef_bet =\<open>א\<close>) \<open>ב\<close>) \<open>ג\<close>) \<open>ד\<close>) \<open>ה\<close>) \<open>ו\<close>) \<open>ז\<close>) \<open>ח\<close>) \<open>ט\<close>) \<open>י\<close>) \<open>כ\<close>) \<open>ל\<close>) \<open>מ\<close>) \<open>נ\<close>) \<open>ס\<close>) \<open>ע\<close>) \<open>פ\<close>) \<open>צ\<close>) \<open>ק\<close>) \<open>ר\<close>) \<open>ש\<close>) \<open>ת\<close>) thm alef_bet.induct\<open>Interpreting Hebrew letters as numbers.\<close> primrec mispar :: "alef_bet \ nat" where "mispar א = 1" "mispar ב = 2" "mispar ג = 3" "mispar ד = 4" "mispar ה = 5" "mispar ו = 6" "mispar ז = 7" "mispar ח = 8" "mispar ט = 9" "mispar י = 10" "mispar כ = 20" "mispar ל = 30" "mispar מ = 40" "mispar נ = 50" "mispar ס = 60" "mispar ע = 70" "mispar פ = 80" "mispar צ = 90" "mispar ק = 100" "mispar ר = 200" "mispar ש = 300" "mispar ת = 400" thm mispar.simpslemma "mispar ק + mispar ל + mispar ה = 135" by simpend quality 97%
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
