namespace http://cds.omdoc.org/examples❚

import lfrules scala://lf.mmt.kwarc.info/❚
import stdlit scala://uom.api.mmt.kwarc.info/❚

/T   a quick, minimal definition of fractional numbers for use in quantities.mmt ❚
theory Real : ur:?LF =
  real: type❙

  plus: real ⟶ real ⟶ real❘ # 1 + 2 prec 10 ❙
  minus : real ⟶ real ⟶ real ❘ # 1 - 2 prec 10 ❙
  times: real ⟶ real ⟶ real❘ # 1 * 2 prec 15❙
  div: real ⟶ real ⟶ real❘ # 1 / 2 prec 15❙
  
  rule lfrules?Realize real stdlit?StandardRat❙
❚