Files

 master

/

thys

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

Andrei Popescu

Merge branch 'master' of github.com:jvanbruegge/binder_datatypes

Mar 27, 2025

9ba5282 · Mar 27, 2025

History

History

/

thys

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
BindingCorecursorCompact		BindingCorecursorCompact	added simpler version of the corecursor proof for lambda co-terms	Mar 27, 2025
Infinitary_FOL		Infinitary_FOL	Fix last remaining issues with new inject theorems	Mar 24, 2025
Infinitary_Lambda_Calculus		Infinitary_Lambda_Calculus	Fix LC and ILC after automatic inject theorems	Mar 24, 2025
Injectivity		Injectivity	more explicit assumptions	Mar 17, 2025
LetRec		LetRec	more	Mar 27, 2025
POPLmark		POPLmark	more	Mar 24, 2025
Pi_Calculus		Pi_Calculus	Fix the process calculus for sugar inject theorems	Mar 24, 2025
Prelim		Prelim	Do not declare bij_implies_inject as simp rule	Dec 18, 2024
STLC		STLC	Fix last remaining issues with new inject theorems	Mar 24, 2025
System_Fc		System_Fc	Register mixfix syntax with constructors	Jul 7, 2024
Untyped_Lambda_Calculus		Untyped_Lambda_Calculus	Fix LC and ILC after automatic inject theorems	Mar 24, 2025
General_Customization.thy		General_Customization.thy	pi almost sorry-free	Jul 5, 2023
Generic_Barendregt_Enhanced_Rule_Induction.thy		Generic_Barendregt_Enhanced_Rule_Induction.thy	Do not declare bij_implies_inject as simp rule	Dec 18, 2024
MRBNF_Composition.thy		MRBNF_Composition.thy	Fix composition for types with no live vars	Aug 1, 2024
MRBNF_FP.thy		MRBNF_FP.thy	Use simp for unfolding induct_forall and induct_implies	Dec 19, 2024
MRBNF_Recursor.thy		MRBNF_Recursor.thy	Provide existential and single-binder inject theorems	Mar 24, 2025
No_Least_Support_Counterexample.thy		No_Least_Support_Counterexample.thy	renamed	Mar 22, 2024
Swapping.thy		Swapping.thy	Fix POPLmark for new inject theorems	Mar 24, 2025
Urban_Berghofer_Norrish_Rule_Induction.thy		Urban_Berghofer_Norrish_Rule_Induction.thy	more	Jul 11, 2024
View all files