Skip to content

Commit

Permalink
tweak
Browse files Browse the repository at this point in the history
  • Loading branch information
jsiek committed Oct 15, 2024
1 parent 7af8657 commit bcc8814
Showing 1 changed file with 7 additions and 4 deletions.
11 changes: 7 additions & 4 deletions index.md
Original file line number Diff line number Diff line change
Expand Up @@ -30,10 +30,8 @@ a position before the index returned by `search(xs, y)`.
function search(List<Nat>, Nat) -> Nat {
search(empty, y) = 0
search(node(x, xs), y) =
if x = y then
0
else
suc(search(xs, y))
if x = y then 0
else suc(search(xs, y))
}
theorem search_take: all xs: List<Nat>. all y:Nat.
Expand Down Expand Up @@ -94,6 +92,11 @@ python -m pip install lark
-->

## Getting Started

The source code for Deduce can be obtained from the following github repository.

[https://github.com/jsiek/deduce](https://github.com/jsiek/deduce)

This introduction to Deduce has two parts. The first part gives a
tutorial on how to write functional programs in Deduce. The second
part shows how to write proofs in Deduce.
Expand Down

0 comments on commit bcc8814

Please sign in to comment.