6 Matching Annotations
 Jul 2018

leanprover.github.io leanprover.github.io

Prove that every natural number can be written as a sum of distinct nonconsecutive 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)


leanprover.github.io leanprover.github.io

Lean’s logic is an even more elaborate and expressive system of logic, which fully subsumes all the notions of higherorder logic we have discussed here.
I would like to know what's that logic ?

 Jun 2018

plato.stanford.edu plato.stanford.edu

Interpretations that give two or more classes for different quantifiers to range over are said to be manysorted, and the classes are sometimes called the sorts.
related to manysorted logic


leanprover.github.io leanprover.github.io

:
here \perp is a symbol of contradiction

 Jan 2018

byorgey.wordpress.com byorgey.wordpress.com

Whereas normal type classes represent predicates on types (each type is either an instance of a type class or it isn’t), multiparameter type classes represent relations on types

 Dec 2017

www.vacationlabs.com www.vacationlabs.com

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 buildtool. Till that day comes, just use Stack.
or
cabal enablenix
now and wait for stablecabal new*
as the future mentioned here
