Completed
CONGRUENCE CLOSURE AND PROOF RELEVANCE
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
The Lean Theorem Prover
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 THE LEAN THEOREM PROVER TEAM
- 3 INTRODUCTION: LEAN
- 4 SECONDARY GOALS
- 5 SOFTWARE VERIFICATION AND FORMALIZED MATHEMATICS
- 6 ARCHITECTURE
- 7 KERNEL
- 8 TWO OFFICIAL LIBRARIES
- 9 AGNOSTIC MATHEMATICS
- 10 FREEDOM TO TRUST
- 11 EXPORTING LIBRARIES
- 12 RECURSIVE EQUATIONS
- 13 TACTICS
- 14 STRUCTURES (ADDITIONAL INSTANCES)
- 15 STRUCTURES (CONCRETE INSTANCES)
- 16 SYLOW THEOREM
- 17 AUTOMATION IN LEAN
- 18 AUTOMATION (MAIN CHALLENGES)
- 19 CASTS
- 20 CONGRUENCE FOR HETEROGENEOUS EQUALITY
- 21 EXAMPLE
- 22 CONGRUENCE CLOSURE AND PROOF RELEVANCE
