function highlight() { var code = document.getElementsByTagName('code'); for (var i = 0; i < code.length; i++) { code[i].innerHTML = code[i].innerHTML .replace(/([(){}→=]+|:|:=)/g, '$1') .replace(/\b(data|transp|∀|Π|Σ|λ|glue|unglue|Glue|hcomp|where|def|mutual|begin|end|module|import|option|false|true|indᵂ|sup|.1|.2|Σ|Π|Pi|Sigma|W|𝟎|𝟏|𝟐|ind₂|ind₁|ind₀|★|0₂|1₂|Path|PathP|Type|Prop|inductive|record|forall|fun|match|let|axiom|type|theorem|lemma|in|U|S|V)\b(?!:)/g, '$1'); } } highlight(); var lastScrollPosition = 0; var ticking = false; var titles = document.querySelector('.header__titles'); var logo = document.querySelector('.header__logo'); function doSomething(scrollPos) { titles.style.transform = 'translate3d(0px, ' + (scrollPos/2) + 'px, 0px)'; logo.style.transform = 'translate3d(0px, ' + (scrollPos/2) + 'px, 0px)'; }