Theory Examples

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Simple examples›

theory Examples
imports Summation_Conversion
begin

ML ‹
  Summation.conv @{context}
  @{cterm "Σ (λq::rat. q ^ Suc (Suc (Suc 0)) + 3) 0 j"}
›

ML ‹
  Summation.conv @{context}
  @{cterm "Σ (λx::real. x ^ Suc (Suc (Suc 0)) + 3) 0 j"}
›

ML ‹
  Summation.conv @{context}
  @{cterm "Σ (λk::int. k ^ Suc (Suc (Suc 0)) + 3) 0 j"}
›

ML ‹
  Summation.conv @{context}
  @{cterm "Σ⇩ℕ (λn::nat. n ^ Suc (Suc (Suc 0)) + 3) 0 m"}
›

end