Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for accessibility predicates based termination checking #2307

Merged
merged 38 commits into from
Jun 3, 2021
Merged

Support for accessibility predicates based termination checking #2307

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
38 commits
Select commit Hold shift + click to select a range
2424569
cp
aseemr May 25, 2021
3f5597c
well-foundnedness of lex and sym
aseemr May 27, 2021
0c6b73b
removing the use of lex ordering, thanks Nik for the suggestion
aseemr May 27, 2021
948961c
Comments and polishing in WellFoundedRelations
aseemr May 28, 2021
6564332
Merge branch 'master' into aseem_misc2
aseemr May 28, 2021
527a7a7
Merge branch 'aseem_misc2' into _aseem_misc
aseemr May 28, 2021
b3272a7
nit
aseemr May 28, 2021
1b83a47
using well-founded relations in the decreases clause to prove ackermann
aseemr May 28, 2021
e651497
use :well-founded syntax
aseemr May 28, 2021
784b515
a cleanup pass
aseemr May 28, 2021
97d7ebf
snap
aseemr May 28, 2021
83d3780
fixing extraction of decreases clauses
aseemr May 28, 2021
456922e
new API For substituting in the decreases clauses
aseemr May 28, 2021
1abbbf8
notes with Nik
aseemr May 28, 2021
668e6e1
snap
aseemr May 28, 2021
f57adab
name change
aseemr May 28, 2021
288edab
interface for lexicographicordering
aseemr May 28, 2021
4c2a25e
reflection API (not supported for wf yet)
aseemr May 31, 2021
3471b09
snap
aseemr May 31, 2021
a748788
bug in printing decreases clauses
aseemr May 31, 2021
6a5f5b4
universe instantiate well_founded_relation
aseemr May 31, 2021
84d5b23
elim_squash in indefinite description
aseemr May 31, 2021
8302c3c
tweaks to well-founded and the lex ackermann example
aseemr May 31, 2021
08dd050
snap
aseemr May 31, 2021
916d8a8
tweak
aseemr May 31, 2021
e82adaf
Merge branch 'master' into _aseem_misc
aseemr May 31, 2021
e9b2e62
tweak
aseemr May 31, 2021
1396d46
tweaks
aseemr May 31, 2021
19a148c
more tweaks
aseemr May 31, 2021
43d386e
some tweaks to the library
aseemr Jun 1, 2021
94de32a
proofs that inverse image and subrelations are well-founded
aseemr Jun 1, 2021
668ca60
Merge branch 'master' into aseem_accessibility_predicates
aseemr Jun 3, 2021
e4d7c4d
handle pretty-printing of well-founded
aseemr Jun 3, 2021
8b71cb5
testcase for pretty-printing decreases
aseemr Jun 3, 2021
9a358bd
snap
aseemr Jun 3, 2021
e97e8f4
streamlining the proofs a bit, re. Nik's PR comments
aseemr Jun 3, 2021
ef15c4d
Merge branch 'master' into aseem_accessibility_predicates
aseemr Jun 3, 2021
f3501f6
Update CHANGES.md
aseemr Jun 3, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
snap
  • Loading branch information
@aseemr
aseemr committed Jun 3, 2021
commit 9a358bdb19d8b57137b2e91273d279893d6e79e4
22 changes: 22 additions & 0 deletions src/ocaml-output/FStar_Parser_ToDocument.ml
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 0 additions & 1 deletion src/parser/parse.fsy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2729,4 +2729,3 @@ in

%%