Skip to content

Release of version 2.0

Compare
Choose a tag to compare
@Yosuke-Ito-345 Yosuke-Ito-345 released this 23 Jul 07:49
· 46 commits to master since this release

Dependencies

  • Coq: v8.13.2
  • MathComp: 1.12.0
  • Coquelicot: 3.1.0

Main changes from version 1.0 to version 2.0

  • Inequalities ">" and ">=" are replaced with "<" and "<=" (advice from ZulipChat).
  • The force of mortality is formalized.
  • Notations "δ", "ω" are changed to "\δ", "\ω" respectively.
  • Some basic lemmas are taken in the "auto" tactic by "Hint Resolve".
  • Generalized the frequency of payments in Premium.v. and Reserve.v.
  • The continuous payment case is newly formalized.