Skip to content

[feat] examples: Add linked-list backed stack#213

Open
ethan-kharitonov wants to merge 1 commit into
awslabs:mainfrom
ethan-kharitonov:uRust-examples/stack
Open

[feat] examples: Add linked-list backed stack#213
ethan-kharitonov wants to merge 1 commit into
awslabs:mainfrom
ethan-kharitonov:uRust-examples/stack

Conversation

@ethan-kharitonov
Copy link
Copy Markdown

@ethan-kharitonov ethan-kharitonov commented Apr 28, 2026

Description of changes: Adds a stack uRust type built on top of the existing linked-list implementation.

  • Stack.thy: stack locale with stack_points_to predicate and verified empty, push, pop, is_empty, and push_all operations.
  • ROOT: Adds Stack theory.

Tested: isabelle build -d . Micro_Rust_Examples.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant