Skip to content

Commit

Permalink
Removing some comments
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Jan 15, 2024
1 parent c80e746 commit 47f6b95
Showing 1 changed file with 2 additions and 15 deletions.
17 changes: 2 additions & 15 deletions tutorial/PulseByExample.fst
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ fn max (n:SZ.t) (a:larray nat (v n))
vmax
}
```
//this option should become the default, once I shake out the handling of address-taking
// This option may become the default at some point
#push-options "--ext 'pulse:rvalues'"
```pulse
fn max_alt (n:SZ.t) (a:larray nat (v n))
Expand Down Expand Up @@ -190,17 +190,4 @@ fn max_alt (n:SZ.t) (a:larray nat (v n))
max
}
```
#pop-options

(*
- some more mature example (e.g. sorting alg)
- some simple record data structure along with a library of functions on this DS
(e.g. library of functions on 2D points)
- build up to explaining the pulse implementation of lpht? -- emphasis on connecting
pure implementation to imperative code
- pulse linked list? -- more traditional sep logic example
- concurrency, e.g. par incr of a ctr
*)
#pop-options

0 comments on commit 47f6b95

Please sign in to comment.