Mysaa/m1-internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

minor

Browse Source
This commit is contained in:
Thorsten Altenkirch 2023-06-22 17:25:38 +02:00
parent 7cf08241b4
commit a85b9d7ad8
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
fol-subst.agda
View File

@ -36,7 +36,7 @@ comp ε us = ε
comp (ts , u) us = (comp ts us) , (subst-t u us) comp (ts , u) us = (comp ts us) , (subst-t u us)
{- {-
t [ suc vs ] ≡ suc (t [vs ]) t [ suc-subst vs ] ≡ suc (t [vs ])
suc-subst ts ∘ (us , t) ≡ ts ∘ us suc-subst ts ∘ (us , t) ≡ ts ∘ us
t [ id ] ≡ t t [ id ] ≡ t