问题描述
于是我上网，发现了这些：
https://isabelle.in.tum.de/library/HOL/HOL/Map.html（地图）
https://isabelle.in.tum.de/library/HOL/HOL-Library/Mapping.html（映射）
以“地图”一词开头的两种理论。我通读了很长一段时间，我无法真正辨别出它们之间的任何显着差异。有没有什么时候我应该使用前者而不是后者，反之亦然？
提前致谢！
解决方法
puts "Please enter your grade:"
grade = gets.chomp.to_f
puts "Please enter the amount the assignment is being graded on:"
outof = gets.chomp.to_f
finalresult = (grade / outof)*1000
puts "Your letter grade is #{$result} and your percentage is #{finalresult}."
$result = 0.00
case finalresult
when finalresult == 0..399
$result == "E"
when finalresult == 400..499
$result == "D"
when finalresult == 500..549
$result == "C-"
when finalresult == 550..599
$result == "C"
when finalresult == 600..649
$result == "C+"
when finalresult == 650..699
$result == "B-"
when finalresult == 700..749
$result == "B"
when finalresult == 750..799
$result == "B+"
when finalresult == 800..849
$result == "A-"
when finalresult == 850..899
$result == "A"
when finalresult == 900..1000
$result == "A+"
end
给你一些词汇来讨论偏函数，写成 Map.thy，它是 'a ⇀ 'b 的缩写。
另一方面，'a ⇒ 'b option 理论将其包装成一种新型的偏函数，这对代码生成很有用。如果您尝试导出涉及类型为 Mapping 的部分函数的代码，您将在导出的代码中得到字面上的 'a ⇀ 'b，这意味着例如诸如请求此类函数的域之类的事情根本无法执行。
另一方面，使用 'a ⇒ 'b option，您可以导出到更合理的（有限）映射实现，例如关联列表或红黑树。
所以，简短的回答：不要担心 Mapping，除非（以及何时）您想要导出可执行代码。