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)
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 ?
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
:
here \perp is a symbol of contradiction
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
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