Mercurial > urweb
comparison demo/prose @ 723:311ca1ae715d
Simplify type class requirement for tree demo
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 13 Apr 2009 08:44:32 -0400 |
| parents | 4e260887d8f2 |
| children | 74a090ff296e |
comparison
equal
deleted
inserted
replaced
| 722:f06880c8bf68 | 723:311ca1ae715d |
|---|---|
| 102 <ol> | 102 <ol> |
| 103 <li> A primary key type <tt>key</tt></li> | 103 <li> A primary key type <tt>key</tt></li> |
| 104 <li> SQL field names <tt>id</tt> (for primary keys) and <tt>parent</tt> (for parent links)</li> | 104 <li> SQL field names <tt>id</tt> (for primary keys) and <tt>parent</tt> (for parent links)</li> |
| 105 <li> A type-level record <tt>cols</tt> of field names besides <tt>id</tt> and <tt>parent</tt></li> | 105 <li> A type-level record <tt>cols</tt> of field names besides <tt>id</tt> and <tt>parent</tt></li> |
| 106 <li> "Proofs" that <tt>id</tt> is distinct from <tt>parent</tt> and that neither of <tt>id</tt> and <tt>parent</tt> appears in <tt>cols</tt></li> | 106 <li> "Proofs" that <tt>id</tt> is distinct from <tt>parent</tt> and that neither of <tt>id</tt> and <tt>parent</tt> appears in <tt>cols</tt></li> |
| 107 <li> Witnesses that both <tt>key</tt> and <tt>option key</tt> belong to the type class <tt>sql_injectable</tt>, which indicates that they are fair game to use with SQL</li> | 107 <li> A witness that <tt>key</tt> belongs to the type class <tt>sql_injectable_prim</tt>, which indicates that both <tt>key</tt> and <tt>option key</tt> are fair game to use with SQL</li> |
| 108 <li> An SQL table <tt>tab</tt>, containing a field <tt>id</tt> of type <tt>key</tt>, a field <tt>parent</tt> of type <tt>option key</tt>, and every field of <tt>cols</tt></li> | 108 <li> An SQL table <tt>tab</tt>, containing a field <tt>id</tt> of type <tt>key</tt>, a field <tt>parent</tt> of type <tt>option key</tt>, and every field of <tt>cols</tt></li> |
| 109 </ol> | 109 </ol> |
| 110 | 110 |
| 111 sum.urp | 111 sum.urp |
| 112 | 112 |