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

Jump to bottom

Adapt to expr.Wf4 #1752

Merged
merged 1 commit into from
Nov 26, 2023
Merged

Adapt to expr.Wf4 #1752

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -640,7 +640,7 @@ For `Language.v`, there is a semi-arbitrary split between two files

- `Wf.v`: Depends on `Inversion.v`
Defines:
+ expr.wf, expr.Wf, expr.wf3, expr.Wf3
+ expr.wf, expr.Wf, expr.wf3, expr.wf4, expr.Wf3, expr.Wf4
+ GeneralizeVar.Flat.wf
+ `expr.inversion_wf` (and variants), which invert `wf` hypotheses
+ `expr.wf_t` (and variants wf_unsafe_t and wf_safe_t) which make
Expand Down
6 changes: 3 additions & 3 deletions src/Language/WfExtra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Module Compilers.
#[global]
Hint Opaque expr.interp expr.Interp : interp_extra.
#[global]
Hint Opaque expr.Wf expr.Wf3 : wf_extra interp_extra.
Hint Opaque expr.Wf expr.Wf3 expr.Wf4 : wf_extra interp_extra.

Module expr.
Import Language.Wf.Compilers.expr.
Expand All @@ -26,8 +26,8 @@ Module Compilers.
Global Hint Opaque expr.APP : wf_extra interp_extra.
#[global]
Hint Rewrite @expr.Interp_APP : interp_extra.
Global Hint Immediate Wf_of_Wf3 : wf_extra.
Global Hint Resolve Wf3_of_Wf : wf_extra.
Global Hint Immediate Wf_of_Wf3 Wf_of_Wf4 : wf_extra.
Global Hint Resolve Wf3_of_Wf Wf4_of_Wf : wf_extra.

Definition Wf_base_Reify_as {t} v
:= @Wf_base_Reify_as base.type.base base.base_interp base.type.base_beq ident ident.buildIdent base.reflect_base_beq t v.
Expand Down
Loading