6 Matching Annotations
1. Jul 2018
2. leanprover.github.io leanprover.github.io
1. Prove that every natural number can be written as a sum of distinct non-consecutive Fibonacci numbers. For example, 22=1+3+5+1322=1+3+5+1322 = 1 + 3 + 5 + 13 is not allowed, since 3 and 5 are consecutive Fibonacci numbers, but 22=1+2122=1+2122 = 1 + 21 is allowed.

Zeckendorf's theorem (first part)

#### URL

3. leanprover.github.io leanprover.github.io
1. Lean’s logic is an even more elaborate and expressive system of logic, which fully subsumes all the notions of higher-order logic we have discussed here.

I would like to know what's that logic ?

#### URL

4. Jun 2018
5. plato.stanford.edu plato.stanford.edu
1. Interpretations that give two or more classes for different quantifiers to range over are said to be many-sorted, and the classes are sometimes called the sorts.

related to many-sorted logic

#### URL

6. leanprover.github.io leanprover.github.io
1. :

here \perp is a symbol of contradiction

#### URL

7. Jan 2018
8. byorgey.wordpress.com byorgey.wordpress.com
1. Whereas normal type classes represent predicates on types (each type is either an instance of a type class or it isn’t), multi-parameter type classes represent relations on types

#### URL

9. Dec 2017
10. www.vacationlabs.com www.vacationlabs.com
1. One hopes, that at some point in the future, the best parts of stack/Stackage and cabal/Hackage can be merged to build a unified, kickass build-tool. Till that day comes, just use Stack.

or `cabal --enable-nix` now and wait for stable `cabal new-*` as the future mentioned here