Files

 master

/

AesopTest

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

jcommelin

and

kim-em

chore: bump toolchain to v4.18.0-rc1 (#201)

Mar 3, 2025

ec060e0 · Mar 3, 2025

History

History

/

AesopTest

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
10.lean		10.lean
12.lean		12.lean
125.lean		125.lean
126.lean		126.lean
13.lean		13.lean
13_2.lean		13_2.lean
18.lean		18.lean
2.lean		2.lean
20.lean		20.lean
23.lean		23.lean
26.lean		26.lean
27.lean		27.lean
41.lean		41.lean
43.lean		43.lean
AddRulesCommand.lean		AddRulesCommand.lean
Aesop.lean		Aesop.lean
AllWeaken.lean		AllWeaken.lean
ApplyHypsTransparency.lean		ApplyHypsTransparency.lean
ApplyTransparency.lean		ApplyTransparency.lean
AssumptionTransparency.lean		AssumptionTransparency.lean
BigStep.lean		BigStep.lean
Cases.lean		Cases.lean
CasesScript.lean		CasesScript.lean
CasesTransparency.lean		CasesTransparency.lean
Com.lean		Com.lean
CompositeLocalRuleTerm.lean		CompositeLocalRuleTerm.lean
ConstructorEquations.lean		ConstructorEquations.lean
Constructors.lean		Constructors.lean
CustomIndexing.lean		CustomIndexing.lean
CustomTactic.lean		CustomTactic.lean
DefaultRuleSets.lean		DefaultRuleSets.lean
DefaultRuleSetsInit.lean		DefaultRuleSetsInit.lean
DestructProducts.lean		DestructProducts.lean
DestructProductsTransparency.lean		DestructProductsTransparency.lean
DocLists.lean		DocLists.lean
DroppedMVars.lean		DroppedMVars.lean
ElabConfig.lean		ElabConfig.lean
EnableUnfold.lean		EnableUnfold.lean
Environment.lean		Environment.lean
EqualUpToIds.lean		EqualUpToIds.lean
Erase.lean		Erase.lean
EraseSimp.lean		EraseSimp.lean
EraseUnfold.lean		EraseUnfold.lean
Ext.lean		Ext.lean
ExtScript.lean		ExtScript.lean
Filter.lean		Filter.lean
Forward.lean		Forward.lean
ForwardConstant.lean		ForwardConstant.lean
ForwardRedundantHypsWithMVars.lean		ForwardRedundantHypsWithMVars.lean
ForwardTransparency.lean		ForwardTransparency.lean
GlobalRuleIdentErrorChecking.lean		GlobalRuleIdentErrorChecking.lean
HeartbeatLimit.lean		HeartbeatLimit.lean
IncompleteScript.lean		IncompleteScript.lean
Intros.lean		Intros.lean
IntrosAllTransparency.lean		IntrosAllTransparency.lean
Jesse.lean		Jesse.lean
LegacyForward.lean		LegacyForward.lean
List.lean		List.lean
LocalRuleSet.lean		LocalRuleSet.lean
LocalTactic.lean		LocalTactic.lean
Logic.lean		Logic.lean
MVarsInInitialGoal.lean		MVarsInInitialGoal.lean
Metas.lean		Metas.lean
NameResolution.lean		NameResolution.lean
NoImportClash.lean		NoImportClash.lean
NoNormSimp.lean		NoNormSimp.lean
NoProgress.lean		NoProgress.lean
Nonterminal.lean		Nonterminal.lean
NormSimp.lean		NormSimp.lean
NormSimpUnchangedMVarAssigned.lean		NormSimpUnchangedMVarAssigned.lean
Persistence0.lean		Persistence0.lean
Persistence1.lean		Persistence1.lean
Persistence2.lean		Persistence2.lean
Persistence3.lean		Persistence3.lean
PostponeSafeRules.lean		PostponeSafeRules.lean
RecursiveUnfoldRule.lean		RecursiveUnfoldRule.lean
RulePattern.lean		RulePattern.lean
RulePatternLooseBVar.lean		RulePatternLooseBVar.lean
RulePatternUniverseBug.lean		RulePatternUniverseBug.lean
RuleSetNameHygiene0.lean		RuleSetNameHygiene0.lean
RuleSetNameHygiene1.lean		RuleSetNameHygiene1.lean
RuleSets0.lean		RuleSets0.lean
RuleSets1.lean		RuleSets1.lean
Safe.lean		Safe.lean
SafeExtractionCopyIntroducedMVars.lean		SafeExtractionCopyIntroducedMVars.lean
SafePrefixExpansionRappLimit.lean		SafePrefixExpansionRappLimit.lean
SafePrefixInTerminalError.lean		SafePrefixInTerminalError.lean
SaturatePerformance.lean		SaturatePerformance.lean
ScriptWithOptions.lean		ScriptWithOptions.lean
SeqCalcProver.lean		SeqCalcProver.lean
SimpLetHypotheses.lean		SimpLetHypotheses.lean
Simprocs.lean		Simprocs.lean
Split.lean		Split.lean
SplitScript.lean		SplitScript.lean
Strategy.lean		Strategy.lean
Subst.lean		Subst.lean
TacGen.lean		TacGen.lean
TacticConfig.lean		TacticConfig.lean
Tauto.lean		Tauto.lean
TerminalError.lean		TerminalError.lean
TraceProof.lean		TraceProof.lean
TryThisIndentation.lean		TryThisIndentation.lean
Unfold.lean		Unfold.lean
UnreachableTacticLinter.lean		UnreachableTacticLinter.lean
WarnApplyIff.lean		WarnApplyIff.lean
View all files