Mercurial > cpdt > repo
comparison src/Match.v @ 437:8077352044b2
A pass over all formatting, after big pile of coqdoc changes
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 27 Jul 2012 16:47:28 -0400 |
parents | 85e743564b22 |
children | 0650420c127b |
comparison
equal
deleted
inserted
replaced
436:5d5e44f905c7 | 437:8077352044b2 |
---|---|
400 (* end thide *) | 400 (* end thide *) |
401 | 401 |
402 (* EX: Write a list map function in Ltac. *) | 402 (* EX: Write a list map function in Ltac. *) |
403 | 403 |
404 (* begin hide *) | 404 (* begin hide *) |
405 (* begin thide *) | |
405 Definition mapp := (map, list). | 406 Definition mapp := (map, list). |
407 (* end thide *) | |
406 (* end hide *) | 408 (* end hide *) |
407 | 409 |
408 (** We can also use anonymous function expressions and local function definitions in Ltac, as this example of a standard list [map] function shows. *) | 410 (** We can also use anonymous function expressions and local function definitions in Ltac, as this example of a standard list [map] function shows. *) |
409 | 411 |
410 (* begin thide *) | 412 (* begin thide *) |