spl alpha-conversion-is-easy issues

spl / alpha-conversion-is-easy

Lean proof of alpha-conversion is easy

4 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Use rcases in places where multiple cases are needed

#39 spl opened 6 years ago
3
Do all update/lam functions fit the same pattern?

#38 spl opened 6 years ago
0
Review naming for of_app, of_lam, etc.

#37 spl closed 6 years ago
6
Rename vname.erase to vname.uninsert

#36 spl opened 6 years ago
1
Consistent naming for `lam` functions that update

#35 spl opened 6 years ago
0
Combine exp.subst.update and exp.subst.update_var

#34 spl closed 6 years ago
0
De Bruijn terms, injections, substitution proof

#33 spl closed 6 years ago
0
Fix psigma decidable_eq in standard library

#32 spl opened 6 years ago
0
Left and right equalities

#31 spl opened 6 years ago
1
Rename aeq.subst to aeq.subst_pres_aeq

#30 spl opened 6 years ago
0
Use same pair notation in vrel and vrel.update

#29 spl opened 6 years ago
0
Use the case tactic instead of commented begin/end for induction and cases

#28 spl opened 6 years ago
0
Show that aexp and substitution forms a category

#27 spl closed 6 years ago
0
Change types from def to structure

#26 spl opened 6 years ago
2
Define functor, applicative, monad instances

#25 spl opened 6 years ago
0
Unify aeq.trans with core into one

#24 spl opened 6 years ago
0
Fix vrel.is_identity instance resolution

#23 spl closed 6 years ago
0
Proposition 6.3

#22 spl opened 6 years ago
2
Proposition 6.2

#21 spl closed 6 years ago
0
Proposition 6.1: identity of subst id

#20 spl closed 6 years ago
0
Alpha-equivalent class of expressions

#19 spl closed 6 years ago
0
Rename vrel.combined to vrel.properties

#18 spl closed 6 years ago
0
Add comments pointing to equivalent propositions in paper

#17 spl closed 6 years ago
0
Create notation for exp.subst as type

#16 spl opened 6 years ago
0
Reorganize exp.subst into multiple files

#15 spl closed 6 years ago
0
Rename iname, oname

#14 spl closed 6 years ago
0
Create new `identity` file for nrel

#13 spl closed 6 years ago
0
Generalize has_fresh class

#12 spl closed 6 years ago
0
Make “core” definitions private?

#11 spl closed 6 years ago
1
Clean up higher-order function implicit parameters

#10 spl closed 6 years ago
0
Clean up top-level variables in each file

#9 spl closed 6 years ago
1
Decide on top-level namespace name

#8 spl closed 6 years ago
0
Clean up naming and notation

#7 spl closed 6 years ago
3
Clean up namespace/section formatting

#6 spl closed 6 years ago
0
Create class for nset

#5 spl closed 6 years ago
0
Rename definition to def and rewrite to rw

#4 spl closed 6 years ago
0
Update to Lean 3

#3 spl closed 6 years ago
0
Define names as a list of nat

#2 spl closed 8 years ago
0
names should be a list

#1 spl closed 8 years ago
1