forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 3
Issues: secure-foundations/dafny
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
well-foundedness check for the datatype 'glinear_fold' feature
glinear
related to glinear
#48
opened Oct 8, 2021 by
tjhance
C++ compilation for consts prevents optimizer from constant-folding
#46
opened Sep 21, 2021 by
tjhance
don't allow uninitialized uses of Something isn't working
shared
bug
#45
opened Sep 17, 2021 by
tjhance
Refining a module method with linear parameters causes linearity errors
#39
opened Aug 17, 2021 by
rtjohnso
be able to 'import opened' a module parameter
modules
the module system
#30
opened Jun 4, 2021 by
tjhance
linear type-checking doesn't handle simultaneity right
good first issue
Good for newcomers
#29
opened May 18, 2021 by
tjhance
glinear updates aren't allowed in ghost context
glinear
related to glinear
#24
opened Apr 9, 2021 by
tjhance
allow linear usage by using all fields
enhancement
New feature or request
#11
opened Dec 15, 2020 by
tjhance
allow existing vars in linear destruct
enhancement
New feature or request
#10
opened Dec 15, 2020 by
tjhance
convenience: do shared borrow in same line as a linear pass
enhancement
New feature or request
#8
opened Dec 2, 2020 by
tjhance
ProTip!
Follow long discussions with comments:>50.