deploy: 30f3348

lean-ja · Nov 4, 2023 · a68cae4 · a68cae4
1 parent 6735a1b
commit a68cae4
Show file tree

Hide file tree

Showing 74 changed files with 423 additions and 231 deletions.
diff --git a/404.html b/404.html
diff --git a/acknowledgments.html b/acknowledgments.html
diff --git a/dependent-types.html b/dependent-types.html
diff --git a/dependent-types/indexed-families.html b/dependent-types/indexed-families.html
diff --git a/dependent-types/indices-parameters-universes.html b/dependent-types/indices-parameters-universes.html
diff --git a/dependent-types/pitfalls.html b/dependent-types/pitfalls.html
diff --git a/dependent-types/summary.html b/dependent-types/summary.html
diff --git a/dependent-types/typed-queries.html b/dependent-types/typed-queries.html
diff --git a/dependent-types/universe-pattern.html b/dependent-types/universe-pattern.html
diff --git a/functor-applicative-monad.html b/functor-applicative-monad.html
diff --git a/functor-applicative-monad/alternative.html b/functor-applicative-monad/alternative.html
diff --git a/functor-applicative-monad/applicative-contract.html b/functor-applicative-monad/applicative-contract.html
diff --git a/functor-applicative-monad/applicative.html b/functor-applicative-monad/applicative.html
diff --git a/functor-applicative-monad/complete.html b/functor-applicative-monad/complete.html
diff --git a/functor-applicative-monad/inheritance.html b/functor-applicative-monad/inheritance.html
diff --git a/functor-applicative-monad/summary.html b/functor-applicative-monad/summary.html
diff --git a/functor-applicative-monad/universes.html b/functor-applicative-monad/universes.html
diff --git a/getting-to-know.html b/getting-to-know.html
diff --git a/getting-to-know/conveniences.html b/getting-to-know/conveniences.html
diff --git a/getting-to-know/datatypes-and-patterns.html b/getting-to-know/datatypes-and-patterns.html
diff --git a/getting-to-know/evaluating.html b/getting-to-know/evaluating.html
diff --git a/getting-to-know/functions-and-definitions.html b/getting-to-know/functions-and-definitions.html
diff --git a/getting-to-know/polymorphism.html b/getting-to-know/polymorphism.html
diff --git a/getting-to-know/structures.html b/getting-to-know/structures.html
diff --git a/getting-to-know/summary.html b/getting-to-know/summary.html
diff --git a/getting-to-know/types.html b/getting-to-know/types.html
diff --git a/hello-world.html b/hello-world.html
diff --git a/hello-world/cat.html b/hello-world/cat.html
diff --git a/hello-world/conveniences.html b/hello-world/conveniences.html
diff --git a/hello-world/running-a-program.html b/hello-world/running-a-program.html
diff --git a/hello-world/starting-a-project.html b/hello-world/starting-a-project.html
diff --git a/hello-world/step-by-step.html b/hello-world/step-by-step.html
diff --git a/hello-world/summary.html b/hello-world/summary.html
diff --git a/index.html b/index.html
diff --git a/introduction.html b/introduction.html
diff --git a/monad-transformers.html b/monad-transformers.html
diff --git a/monad-transformers/conveniences.html b/monad-transformers/conveniences.html
diff --git a/monad-transformers/do.html b/monad-transformers/do.html
diff --git a/monad-transformers/order.html b/monad-transformers/order.html
diff --git a/monad-transformers/reader-io.html b/monad-transformers/reader-io.html
diff --git a/monad-transformers/summary.html b/monad-transformers/summary.html
diff --git a/monad-transformers/transformers.html b/monad-transformers/transformers.html
diff --git a/monads.html b/monads.html
diff --git a/monads/arithmetic.html b/monads/arithmetic.html
diff --git a/monads/class.html b/monads/class.html
diff --git a/monads/conveniences.html b/monads/conveniences.html
diff --git a/monads/do.html b/monads/do.html
diff --git a/monads/io.html b/monads/io.html
diff --git a/monads/summary.html b/monads/summary.html
diff --git a/next-steps.html b/next-steps.html
diff --git a/print.html b/print.html
diff --git a/programs-proofs.html b/programs-proofs.html
diff --git a/programs-proofs/arrays-termination.html b/programs-proofs/arrays-termination.html
diff --git a/programs-proofs/fin.html b/programs-proofs/fin.html
diff --git a/programs-proofs/inequalities.html b/programs-proofs/inequalities.html
diff --git a/programs-proofs/insertion-sort.html b/programs-proofs/insertion-sort.html
diff --git a/programs-proofs/special-types.html b/programs-proofs/special-types.html
diff --git a/programs-proofs/summary.html b/programs-proofs/summary.html
diff --git a/programs-proofs/tail-recursion-proofs.html b/programs-proofs/tail-recursion-proofs.html
diff --git a/programs-proofs/tail-recursion.html b/programs-proofs/tail-recursion.html
diff --git a/props-proofs-indexing.html b/props-proofs-indexing.html
diff --git a/searchindex.js b/searchindex.js
diff --git a/searchindex.json b/searchindex.json
diff --git a/tactics-induction-proofs.html b/tactics-induction-proofs.html
diff --git a/title.html b/title.html
diff --git a/type-classes.html b/type-classes.html
diff --git a/type-classes/coercion.html b/type-classes/coercion.html
diff --git a/type-classes/conveniences.html b/type-classes/conveniences.html
diff --git a/type-classes/indexing.html b/type-classes/indexing.html
diff --git a/type-classes/out-params.html b/type-classes/out-params.html
diff --git a/type-classes/polymorphism.html b/type-classes/polymorphism.html
diff --git a/type-classes/pos.html b/type-classes/pos.html
diff --git a/type-classes/standard-classes.html b/type-classes/standard-classes.html
diff --git a/type-classes/summary.html b/type-classes/summary.html