Menu ▾ ▴

#2 Lists (inductive and polymorphic)

Rodin_2.0
open
nobody
Collections (2)
5
2010-11-17
2010-11-17
Nicolas Beauger
No

An inductive and generic definition of the List type:

List(T) ::=
nil
| cons ( head : T, tail : List(T) )

No proof obligation, hence no proof in the archive.

Discussion

  • Nicolas Beauger

    Nicolas Beauger - 2010-11-17

    List datatype, .tuf file at archive root

     
    Lists.zip

  • Nicolas Beauger

    Nicolas Beauger - 2010-11-17
    • summary: Lists (inductive and generic) --> Lists (inductive and polymorphic)
     

Log in to post a comment.