Issues
- 1
- 0
- 1
- 0
Make `inv` complete on its domain?
#154 opened - 0
Calling lemmas in ghost code
#151 opened - 1
admit seems to affect code before it
#149 opened - 2
Bad error messages
#146 opened - 0
Stack references are freeable
#145 opened - 0
Ghost, Unobservable, Atomic
#144 opened - 1
Recursive calls fail to infer
#141 opened - 1
Meta issue for syntax improvements in Pulse
#139 opened - 1
Eliminating pure underneath an exists*
#137 opened - 4
- 1
Inferred reveal is incorrectly accepted
#113 opened - 1
Interpret `**` on both sides of `@==>` to allow inferring implicit arguments to stick lemmas
#111 opened - 1
- 0
- 1
- 1
- 0
- 1
- 0
- 0
- 0
- 0
Trouble with dependent tuples
#76 opened - 2
Support universe polymorphism
#72 opened - 1
- 0
Bad error localization
#68 opened - 0
- 1
Impossible! (Tm_match)
#62 opened - 0
- 1
Failing smt queries
#57 opened - 4
- 1
SMT query batching
#53 opened - 1
Stack allocated arrays
#52 opened - 2
General recursion in Pulse
#51 opened - 1
Support for predicate syntax in Pulse
#50 opened - 0
Support for interfaces with Pulse
#49 opened - 1
return_stt_ghost_noeq
#47 opened - 1
- 1
Ghost admits do not work
#43 opened - 0
- 0
- 0
- 0
- 2
- 2
Pulse cannot infer permission on record field when permission involves existential quantification
#35 opened - 2
Move Pulse libraries to lib/steel/pulse
#33 opened - 0
- 1