Skip to content

Commit

Permalink
reformat
Browse files Browse the repository at this point in the history
  • Loading branch information
jsiek committed Jan 22, 2025
1 parent 7f8c67f commit 9dbc3a2
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions gh-pages/deduce-code/home_example2.pf
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,9 @@ proof
arbitrary x:Nat, y:Nat
assume: x < y
assume: x = y
have: y < y by rewrite (recall x = y) in recall x < y
have: y < y by rewrite (recall x = y)
in recall x < y
have: not (y < y) by less_irreflexive
conclude false by apply (recall not (y < y)) to recall y < y
conclude false by apply (recall not (y < y))
to recall y < y
end

0 comments on commit 9dbc3a2

Please sign in to comment.