Mercurial > cpdt > repo
comparison src/Coinductive.v @ 436:5d5e44f905c7
Changes during more coqdoc hacking
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 27 Jul 2012 15:41:06 -0400 |
| parents | a54a4a2ea6e4 |
| children | 8077352044b2 |
comparison
equal
deleted
inserted
replaced
| 435:a54a4a2ea6e4 | 436:5d5e44f905c7 |
|---|---|
| 541 | 541 |
| 542 We define a suggestive synonym for [nat], as we will consider programs with infinitely many variables, represented as [nat]s. *) | 542 We define a suggestive synonym for [nat], as we will consider programs with infinitely many variables, represented as [nat]s. *) |
| 543 | 543 |
| 544 Definition var := nat. | 544 Definition var := nat. |
| 545 | 545 |
| 546 (** We define a type [vars] of maps from variables to values. To define a function [set] for setting a variable's value in a map, we import the [Arith] module from Coq's standard library, and we use its function [beq_nat] for comparing natural numbers. *) | 546 (** We define a type [vars] of maps from variables to values. To define a function [set] for setting a variable's value in a map, we use the standard library function [beq_nat] for comparing natural numbers. *) |
| 547 | 547 |
| 548 Definition vars := var -> nat. | 548 Definition vars := var -> nat. |
| 549 Require Import Arith. | |
| 550 Definition set (vs : vars) (v : var) (n : nat) : vars := | 549 Definition set (vs : vars) (v : var) (n : nat) : vars := |
| 551 fun v' => if beq_nat v v' then n else vs v'. | 550 fun v' => if beq_nat v v' then n else vs v'. |
| 552 | 551 |
| 553 (** We define a simple arithmetic expression language with variables, and we give it a semantics via an interpreter. *) | 552 (** We define a simple arithmetic expression language with variables, and we give it a semantics via an interpreter. *) |
| 554 | 553 |