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

Exploration towards including #311 in Coq #316

Draft
wants to merge 8 commits into
base: master
Choose a base branch
from
Draft

Exploration towards including #311 in Coq #316

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
41a84c8
spec: subtype checking only for reference types
chenyan-dfinity Jan 12, 2022
b451027
use inference rule instead of partial function
chenyan-dfinity Jan 13, 2022
fa36bc0
Apply suggestions from code review
chenyan-dfinity Jan 13, 2022
a9a03b4
fix
chenyan-dfinity Jan 13, 2022
20b84d1
Merge branch 'master' into spec-variant
chenyan-dfinity Jan 14, 2022
cb6fce7
Exploration towards including #311 in Coq
nomeata Feb 10, 2022
2b71d78
Some more experiments, but still not good
nomeata Feb 19, 2022
12da438
Introduce type environment for refs; a bit of progress
nomeata Apr 7, 2022
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
Loading