michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Make Γ and A parameters instead of indices to the _—↠_ relation (#539)

Browse source
This commit is contained in:
Marko Dimjašević 2020-10-24 17:01:09 +02:00 committed by GitHub
parent f0ca07c371
commit 2db6d7754f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/plfa/part2/DeBruijn.lagda.md
View file

@ -874,13 +874,13 @@ infix 1 begin_
infixr 2 _—→⟨_⟩_ infixr 2 _—→⟨_⟩_
infix 3 _∎ infix 3 _∎
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
_∎ : ∀ {Γ A} (M : Γ ⊢ A) _∎ : (M : Γ ⊢ A)
------ ------
→ M —↠ M → M —↠ M
_—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A} _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
→ L —→ M → L —→ M
→ M —↠ N → M —↠ N
------ ------

6
src/plfa/part2/More.lagda.md
View file

@ -989,13 +989,13 @@ infix 1 begin_
infixr 2 _—→⟨_⟩_ infixr 2 _—→⟨_⟩_
infix 3 _∎ infix 3 _∎
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
_∎ : ∀ {Γ A} (M : Γ ⊢ A) _∎ : (M : Γ ⊢ A)
------ ------
→ M —↠ M → M —↠ M
_—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A} _—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
→ L —→ M → L —→ M
→ M —↠ N → M —↠ N
------ ------