pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-12 17:17:50 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising before class

Browse source
This commit is contained in:
Adam Chlipala 2020-04-08 10:48:14 -04:00
parent 583605fded
commit ca3a490119
4 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
DeepAndShallowEmbeddings.v
View file

@ -332,7 +332,7 @@ Module Deep.
| Write (a v : nat) : cmd unit.
(* These constructors are most easily explained through examples. We'll
* translate both of the programs from the shallowly embedding above. *)
* translate both of the programs from the shallow embedding above. *)
Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80).

2
DeepInterp.ml
View file

@ -1,3 +1,5 @@
open Deep
let rec i2n n =
match n with
| 0 -> O

2
DeeperInterp.ml
View file

@ -1,3 +1,5 @@
open Deeper
let rec i2n n =
match n with
| 0 -> O

2
DeeperWithFailInterp.ml
View file

@ -1,3 +1,5 @@
open DeeperWithFail
let rec i2n n =
match n with
| 0 -> O