Issues
- 0
Repeating proofs for unbox_fetch and get_here
#34 opened by Ayertienna - 2
Comment the code!
#20 opened by Ayertienna - 1
How to make automatic rewrites of hypothesis?
#23 opened by Ayertienna - 3
Reducibility properties + normalization
#24 opened by Ayertienna - 1
Documentation cleanup
#32 opened by Ayertienna - 1
Document language equivalence
#31 opened by Ayertienna - 1
Document strong normalization
#26 opened by Ayertienna - 2
Document implementation details
#25 opened by Ayertienna - 2
labeled -> label-free typing
#14 opened by Ayertienna - 2
label-free -> labeled typing
#13 opened by Ayertienna - 1
Finish (mosty term) rewrites
#12 opened by Ayertienna - 2
All the small lemmas... - lang. equiv.
#10 opened by Ayertienna - 1
- 1
L_to_Hyb: dynamics
#45 opened by Ayertienna - 1
L_to_Hyb: final version for statics
#46 opened by Ayertienna - 2
L_to_Hyb: shifting problems
#47 opened by Ayertienna - 2
shift_term_Hyb + typing
#48 opened by Ayertienna - 1
L_to_Hyb: try one more thing
#49 opened by Ayertienna - 4
Module dependencies
#15 opened by Ayertienna - 9
Remove all 'skip' & 'Admitted' from the code
#36 opened by Ayertienna - 2
Decision procedure: permut
#38 opened by Ayertienna - 1
permut_app_inv (PermutLib.v)
#39 opened by Ayertienna - 1
ok_LF + permutation = more concrete matching
#42 opened by Ayertienna - 1
Adding fresh type variable
#41 opened by Ayertienna - 3
Rewrite labeled version
#30 opened by Ayertienna - 5
permut from tlc or Permutation from stdlib?
#19 opened by Ayertienna - 1
LLOkLib library
#43 opened by Ayertienna - 1
ok_LF is preserved under permutation
#40 opened by Ayertienna - 3
Tactics for ok_Bg
#6 opened by Ayertienna - 2
Tactics for emptyEquiv
#7 opened by Ayertienna - 0
- 1
Slowdown of eauto
#35 opened by Ayertienna - 3
Tactics for permut
#5 opened by Ayertienna - 1
Wrong definitions of locally_closed
#37 opened by Ayertienna - 2
Metatheory upgrade
#16 opened by Ayertienna - 1
Split repo
#28 opened by Ayertienna - 1
Env vs lists
#29 opened by Ayertienna - 1
Merge LN into master
#27 opened by Ayertienna - 1
- 1
Automate proofs
#1 opened by Ayertienna - 1
- 1
- 1
- 1
Rewrite from Omega, Gamma to G, (w, Gamma_w)
#11 opened by Ayertienna - 1
Labeled language implementation details
#17 opened by Ayertienna - 0
Label-free language implementation details
#18 opened by Ayertienna - 3
Reconsider using inductive definition of subst_t instead of fixpoint for label-free
#21 opened by Ayertienna - 2
- 2
Problem with context substitution (renaming)
#22 opened by Ayertienna