Demo entry 5747125

List

   

Submitted by bla on Jul 12, 2016 at 13:54
Language: Isabelle. Code size: 312 Bytes.

theory List
imports Plain Presburger Code_Numeral Quotient ATP
begin

datatype 'a list =
    Nil    ("[]")
  | Cons 'a  "'a list"    (infixr "#" 65)

syntax
  -- {* list Enumeration *}
  "_list" :: "args => 'a list"    ("[(_)]")

translations
  "[x, xs]" == "x#[xs]"
  "[x]" == "x#[]"
(*...*)
end

This snippet took 0.00 seconds to highlight.

Back to the Entry List or Home.

Delete this entry (admin only).