FormalizedFormalLogic/Foundation

code:cloc

cloc --by-file .

114 text files.

114 unique files.

0 files ignored.

github.com/AlDanial/cloc v 1.98 T=0.08 s (1417.2 files/s, 343825.6 lines/s)

----------------------------------------------------------------------------------------------------

File blank comment code

----------------------------------------------------------------------------------------------------

./FirstOrder/Basic/Syntax/Rew.lean 367 44 894

./Modal/System.lean 380 4 810

./Vorspiel/Vorspiel.lean 239 1 600

./Logic/HilbertStyle/Supplemental.lean 179 10 599

./Modal/ConsistentTheory.lean 75 3 530

./FirstOrder/Basic/Semantics/Semantics.lean 201 4 521

./Vorspiel/Arith.lean 104 0 463

./Modal/Kripke/Semantics.lean 138 0 462

./Logic/LogicSymbol.lean 234 15 442

./FirstOrder/Basic/Syntax/Formula.lean 177 14 435

./FirstOrder/Basic/BinderNotation.lean 61 0 420

./FirstOrder/Basic/Operator.lean 210 1 413

./Modal/Hilbert.lean 124 14 379

./Logic/System.lean 237 17 369

./FirstOrder/Basic/Calculus.lean 126 83 364

./IntProp/ConsistentTableau.lean 88 0 362

./IntProp/Kripke/Semantics.lean 136 0 361

./FirstOrder/Arith/Hierarchy.lean 65 0 360

./Modal/Complemental.lean 83 0 357

./FirstOrder/Basic/Syntax/Language.lean 131 43 324

./Modal/Formula.lean 130 76 312

./Modal/Kripke/Geach.lean 97 0 311

./FirstOrder/Arith/Representation.lean 56 43 295

./IntProp/Kripke/Completeness.lean 53 3 290

./Modal/LogicSymbol.lean 200 1 287

./Logic/HilbertStyle/Basic.lean 135 5 286

./FirstOrder/Completeness/SearchTree.lean 62 0 274

./Modal/Kripke/Filteration.lean 61 1 261

./Modal/Kripke/Grz/Completeness.lean 39 2 243

./Logic/HilbertStyle/Context.lean 142 0 216

./FirstOrder/Basic/Eq.lean 94 0 210

./Logic/Kripke/Preservation.lean 77 0 208

./IntProp/Formula.lean 37 1 200

./Modal/Maximal.lean 51 4 194

./Logic/Kripke/Tree.lean 59 0 193

./FirstOrder/Completeness/SubLanguage.lean 55 0 192

./Logic/Semantics.lean 91 12 187

./Modal/Kripke/Grz/Definability.lean 27 1 178

./Modal/Kripke/GL/Completeness.lean 23 0 176

./FirstOrder/Arith/Basic.lean 88 0 175

./FirstOrder/Arith/Model.lean 70 0 173

./Propositional/Classical/Basic/Completeness.lean 33 0 163

./FirstOrder/Basic/Semantics/Elementary.lean 75 0 162

./Modal/Kripke/Completeness.lean 40 2 161

./Modal/Kripke/GL/Tree.lean 51 6 157

./Logic/LindenbaumAlgebra.lean 50 0 156

./IntProp/Deduction.lean 54 6 155

./Modal/Kripke/GL/MDP.lean 33 0 155

./FirstOrder/Arith/PeanoMinus.lean 45 0 154

./Propositional/Classical/Basic/Formula.lean 49 0 152

./Logic/Kripke/Basic.lean 88 22 149

./FirstOrder/Interpretation.lean 51 1 147

./Logic/HilbertStyle/Lukasiewicz.lean 52 1 138

./FirstOrder/Basic/Syntax/Term.lean 76 6 135

./FirstOrder/Basic/Coding.lean 18 0 134

./FirstOrder/Basic/Model.lean 68 0 133

./Vorspiel/BinaryRelations.lean 49 7 133

./IntProp/Kripke/DP.lean 17 0 130

./Logic/Calculus.lean 68 35 130

./Modal/PLoN/Semantics.lean 81 0 128

./Modal/Boxdot/GL_Grz.lean 17 0 127

./Modal/Geach.lean 63 0 125

./Propositional/Classical/Basic/Calculus.lean 30 0 125

./FirstOrder/Ultraproduct.lean 41 0 119

./IntProp/Heyting/Semantics.lean 57 0 111

./IntProp/Kripke/LEM.lean 29 11 106

./Modal/Kripke/Dot3.lean 18 0 106

./Modal/Kripke/GL/Definability.lean 14 0 104

./FirstOrder/Arith/CobhamR0.lean 25 0 92

./Modal/ModalCompanion/Basic.lean 19 1 87

./FirstOrder/Basic/Calculus2.lean 21 4 77

./Modal/Kripke/Preservation.lean 26 0 76

./FirstOrder/Basic/Soundness.lean 18 0 74

./Modal/Kripke/ComplexityLimited.lean 10 0 74

./FirstOrder/Arith/Nonstandard.lean 28 0 73

./Vorspiel/Collection.lean 43 0 69

./Logic/Kripke/Closure.lean 52 0 68

./FirstOrder/Arith/Theory.lean 37 0 66

./FirstOrder/Completeness/Completeness.lean 23 0 66

./Modal/Axioms.lean 25 3 65

./FirstOrder/Completeness/Coding.lean 17 0 63

./IntProp/Dialectica/Basic.lean 28 4 63

./AutoProver/Litform.lean 21 0 62

./Modal/PLoN/Completeness.lean 14 0 62

./FirstOrder/Arith/StrictHierarchy.lean 15 0 59

./Modal/Boxdot/Basic.lean 14 0 49

./Propositional/Classical/Basic/Semantics.lean 24 0 49

./Logic/Axioms.lean 22 0 48

./Modal/ModalCompanion/GMT.lean 10 0 45

./Vorspiel/Order.lean 14 0 41

./Logic/Kripke/RelItr.lean 9 0 37

./Modal/Kripke/Ver.lean 15 0 37

./FirstOrder/Completeness/Corollaries.lean 13 0 26

./FirstOrder/Order/Le.lean 12 0 26

./Logic/Disjunctive.lean 7 0 23

./Modal/PLoN/Soundness.lean 13 0 21

./Modal/MDP.lean 9 0 20

./Vorspiel/String.lean 5 0 20

./Modal/Kripke/S5.lean 8 0 19

./FirstOrder/Basic.lean 0 0 14

./Modal/Kripke/Kripke.lean 2 0 10

./Vorspiel/ExistsUnique.lean 6 0 9

./Vorspiel/NotationClass.lean 6 2 9

./Vorspiel/Meta.lean 108 401 6

./Modal/Modal.lean 0 0 5

./Propositional/Classical/Basic.lean 0 0 4

./IntProp/IntProp.lean 0 0 3

./IntProp/Kripke/Kripke.lean 0 0 3

./Modal/Kripke/GL/GL.lean 0 0 3

./Modal/PLoN/PLoN.lean 0 0 3

./Logic/Init.lean 1 0 2

./Modal/Boxdot/Boxdot.lean 0 0 2

./Modal/Kripke/Grz/Grz.lean 0 0 2

./Modal/ModalCompanion/ModalCompanion.lean 0 0 2

----------------------------------------------------------------------------------------------------

SUM: 6989 914 19755

----------------------------------------------------------------------------------------------------