yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Finish refactoring logical relations

Browse source
This commit is contained in:
Yiyun Liu 2025-03-03 01:15:21 -05:00
parent 7f38544a1e
commit 47e21df801
2 changed files with 318 additions and 376 deletions
Download patch file Download diff file Expand all files Collapse all files

2
theories/common.v
View file

@ -10,6 +10,8 @@ Inductive lookup : nat -> list PTm -> PTm -> Prop :=
lookup i Γ A ->
lookup (S i) (cons B Γ) (ren_PTm shift A).
Derive Inversion lookup_inv with (forall i Γ A, lookup i Γ A).
Definition renaming_ok (Γ : list PTm) (Δ : list PTm) (ξ : nat -> nat) :=
forall i A, lookup i Δ A -> lookup (ξ i) Γ (ren_PTm ξ A).

692
theories/logrel.v
View file

File diff suppressed because it is too large Load diff