diff --git a/nav.js b/nav.js
index fe1a170..895cdc7 100644
--- a/nav.js
+++ b/nav.js
@@ -26,124 +26,245 @@ for (const elem of document.getElementsByClassName('nav_sect')) {
 }
 
 for (const currentFileLink of document.getElementsByClassName('visible')) {
-  currentFileLink.scrollIntoView({block: 'center'});
+  currentFileLink.scrollIntoView({ block: 'center' });
 }
 
-
-
-
-
-
 // Tactic list tag filter
-// ----------------------
+// ---------------------- 
 
-function filterSelectionClass(tagNames, classname) {
-    if (tagNames.length == 0) {
-      for (const elem of document.getElementsByClassName(classname)) {
-        elem.classList.remove("hide");
-      }
-    } else {
-      // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
-      for (const elem of document.getElementsByClassName(classname)) {
-        elem.classList.add("hide");
-        for (const tagName of tagNames) {
-            if (elem.classList.contains(tagName)) {
-              elem.classList.remove("hide");
-            }
+function filterSelectionClass(tagNames, className) {
+  if (tagNames.length === 0) {
+    for (const elem of document.getElementsByClassName(className)) {
+      elem.classList.remove("hide");
+    }
+  } else {
+    // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
+    for (const elem of document.getElementsByClassName(className)) {
+      elem.classList.add("hide");
+      for (const tagName of tagNames) {
+        if (elem.classList.contains(tagName)) {
+          elem.classList.remove("hide");
         }
       }
     }
   }
+}
 
-  function filterSelection(c) {
-    filterSelectionClass(c, "tactic");
-    filterSelectionClass(c, "taclink");
-  }
+function filterSelection(c) {
+  filterSelectionClass(c, "tactic");
+  filterSelectionClass(c, "taclink");
+}
 
-var filterBoxes = document.getElementsByClassName("tagfilter");
+var filterBoxesElmnts = document.getElementsByClassName("tagfilter");
 
 function updateDisplay() {
-    filterSelection(getSelectValues());
+  filterSelection(getSelectValues());
 }
 
 function getSelectValues() {
-    var result = [];
-
-    for (const opt of filterBoxes) {
-
-      if (opt.checked) {
-        result.push(opt.value);
-      }
+  var result = [];
+  for (const opt of filterBoxesElmnts) {
+    if (opt.checked) {
+      result.push(opt.value);
     }
-    return result;
   }
+  return result;
+}
 
 function setSelectVal(val) {
-  for (const opt of filterBoxes) {
+  for (const opt of filterBoxesElmnts) {
     opt.checked = val;
   }
 }
 
 updateDisplay();
 
-for (const opt of filterBoxes) {
+for (const opt of filterBoxesElmnts) {
   opt.addEventListener('change', updateDisplay);
 }
 
-const tse = document.getElementById("tagfilter-selectall")
-if (tse != null) {
-  tse.addEventListener('change', function() {
+const tse = document.getElementById("tagfilter-selectall");
+if (tse !== null) {
+  tse.addEventListener('change', function () {
     setSelectVal(this.checked);
     updateDisplay();
   });
 }
 
+// Simple search through declarations by name, file name and description comment as printed from mathlib
+// -------------------------
+const MAX_COUNT_RESULTS = 10;
 
+/* Get all elements for searching and showing results */
+const searchForm = document.getElementById('search_form');
+const searchQueryInput = searchForm.querySelector('input[name=query]');
+const searchResultsContainer = document.getElementById('search_results');
 
+/* Handle opening/closing search results container */
+function closeResultsDisplay() {
+  searchResultsContainer.style.display = 'none';
+}
 
+function openResultsDisplay() {
+  searchResultsContainer.style.display = 'block';
+}
 
+/* Handle resizing search results container */
+const SMALL = 'condensed';
+const LARGE = 'full_width';
+function renderSmallResultsContainer() {
+  searchResultsContainer.classList.contains(LARGE) 
+  ? 
+    searchResultsContainer.classList.contains(SMALL) 
+    ?
+      searchResultsContainer.classList.remove(LARGE) 
+    :
+      searchResultsContainer.classList.replace(LARGE, SMALL) 
+  : 
+    !searchResultsContainer.classList.contains(SMALL) && searchResultsContainer.classList.add(SMALL);
+}
 
-// Simple declaration search
-// -------------------------
+function renderLargeResultsContainer() {
+  searchResultsContainer.classList.contains(SMALL) 
+  ? 
+    searchResultsContainer.classList.contains(LARGE) 
+    ?
+      searchResultsContainer.classList.remove(SMALL) 
+    :
+      searchResultsContainer.classList.replace(SMALL, LARGE) 
+  : 
+    !searchResultsContainer.classList.contains(LARGE) && searchResultsContainer.classList.add(LARGE);
+}
+/* Set up defaults for search filtering and results */ 
+const filters = {
+  attributes: [],
+  kind: []
+};
 
+/* Handle searching through the index with a specific query and filters */
 const searchWorkerURL = new URL(`${siteRoot}searchWorker.js`, window.location);
-const declSearch = (q) => new Promise((resolve, reject) => {
-  const worker = new SharedWorker(searchWorkerURL);
+const worker = new SharedWorker(searchWorkerURL);
+const searchIndexedData = (query, maxResultsCount) => new Promise((resolve, reject) => {
+  const maxCount = typeof maxResultsCount === "number" ? maxResultsCount : MAX_COUNT_RESULTS;
+
   worker.port.start();
-  worker.port.onmessage = ({data}) => resolve(data);
+  worker.port.onmessage = ({ data }) => resolve(data);
   worker.port.onmessageerror = (e) => reject(e);
-  worker.port.postMessage({q});
+  worker.port.postMessage({ query, maxCount, filters });
 });
 
-const srId = 'search_results';
-document.getElementById('search_form')
-  .appendChild(document.createElement('div'))
-  .id = srId;
-
-function handleSearchCursorUpDown(down) {
-  const sel = document.querySelector(`#${srId} .selected`);
-  const sr = document.getElementById(srId);
-  if (sel) {
-    sel.classList.remove('selected');
-    const toSelect = down ?
-      sel.nextSibling || sr.firstChild:
-      sel.previousSibling || sr.lastChild;
-    toSelect && toSelect.classList.add('selected');
-  } else {
-    const toSelect = down ? sr.firstChild : sr.lastChild;
-    toSelect && toSelect.classList.add('selected');
+/* Submitting search query */
+const submitSearchFormHandler = async (ev) => {
+  ev?.preventDefault();
+  closeFiltersDisplay();
+  
+  const query = searchQueryInput.value;
+  if (!query || query.length <= 0) {
+    closeResultsDisplay();
+    return;
   }
+  renderSmallResultsContainer();
+  openResultsDisplay();
+
+
+  searchResultsContainer.setAttribute('state', 'loading');
+  await fillInSearchResultsContainer(query);
+  searchResultsContainer.setAttribute('state', 'done');
+
+  const searchResultsContainerCloseBtn = document.getElementById('close_results_btn');
+  searchResultsContainerCloseBtn?.addEventListener("click", closeResultsDisplay);
+
+  const searchResultsShowAllBtn = document.getElementById('show_all_results_btn');
+  searchResultsShowAllBtn?.addEventListener('click', () => renderAllResultsHtml(query));
+};
+searchForm.addEventListener('submit', submitSearchFormHandler);
+
+const renderAllResultsHtml = async (query) => {
+  if (!query && query.length <= 0) {
+    closeResultsDisplay();
+    return;
+  }
+
+  searchResultsContainer.setAttribute('state', 'loading');
+  await fillInSearchResultsContainer(query, true);
+  
+  renderLargeResultsContainer();
+  openResultsDisplay();
+  searchResultsContainer.setAttribute('state', 'done');
+
+  const searchResultsContainerCloseBtn = document.getElementById('close_results_btn');
+  searchResultsContainerCloseBtn?.addEventListener("click", closeResultsDisplay);
+}
+
+const fillInSearchResultsContainer = async (query, showAll = false) => {
+  searchResultsContainer.innerHTML = '';
+  const resultsCount = showAll ? -1 : MAX_COUNT_RESULTS;
+  const {response: results, total} = await searchIndexedData(query, resultsCount);
+  results.sort((a, b) => (a && typeof a.score === "number" && b && typeof b.score === "number") ? (b.score - a.score) : 0);
+
+  const searchResultsCloseBtn = '<span class="close" id="close_results_btn">x</span>';
+  searchResultsContainer.innerHTML = results.length < 1 ? createNoResultsHTML(searchResultsCloseBtn) : createResultsHTML(results, total, showAll, searchResultsCloseBtn);
 }
 
-function handleSearchEnter() {
-  const sel = document.querySelector(`#${srId} .selected`)
-    || document.getElementById(srId).firstChild;
-  sel.click();
+const createNoResultsHTML = (html) => `<p class="no_search_result"> No declarations or comments match your search. </p>${html}`;
+
+const createResultsHTML = (results, total, showAll, html) => {
+  const descriptionMaxLength = showAll ? 350 : 80;
+  const countShowingResults = MAX_COUNT_RESULTS > results.length ? results.length : MAX_COUNT_RESULTS;
+
+  let resultHtml = `<p id="search_info">Found ${total} matches 
+    ${!showAll ?
+      `, showing ${countShowingResults}.</p><span id="show_all_results_btn" class="link_coloring">Show all</span>` :
+      ''
+    }
+  ${html}`;
+  resultHtml += results.map((result, index) => {
+    return createSingleResultHTML(result, descriptionMaxLength, index);
+  }).join('');
+  return resultHtml;
 }
 
-const searchInput = document.querySelector('#search_form input[name=q]');
+const createSingleResultHTML = (result, descriptionMaxLength, i) => {
+  const { module, name, description } = result;
+  const resultUrl = `${siteRoot}${module}#${name}`;
+  const descriptionDisplay = description && description.length > 0 ? 
+    `${description.slice(0, descriptionMaxLength)}${description.length > descriptionMaxLength ? '..' : ''}` :
+    '';
+
+  const html = `<div id="search_result_${i}" class="search_result_item">
+    <a href="${resultUrl}" class="search_result_anchor">
+      <b class="result_name">${name}</b>
+      <br>
+      <p class="result_module">${module}</p>
+      <p class="result_comment">${descriptionDisplay}</p>
+    </a>
+  </div>`;
+
+	return html;
+} 
+
+/* Keyboard navigation through search input and results */
+searchQueryInput.addEventListener('keydown', (ev) => {
+  if (!searchQueryInput.value || searchQueryInput.value.length === 0) {
+    searchResultsContainer.innerHTML = '';
+  } else {
+    switch (ev.key) {
+      case 'Down':
+      case 'ArrowDown':
+        ev.preventDefault();
+        handleSearchCursorUpDown(true);
+        break;
+      case 'Up':
+      case 'ArrowUp':
+        ev.preventDefault();
+        handleSearchCursorUpDown(false);
+        break;
+    }
+  }
+  
+});
 
-searchInput.addEventListener('keydown', (ev) => {
+searchResultsContainer.addEventListener('keydown', (ev) => {
   switch (ev.key) {
     case 'Down':
     case 'ArrowDown':
@@ -157,65 +278,105 @@ searchInput.addEventListener('keydown', (ev) => {
       break;
     case 'Enter':
       ev.preventDefault();
-      handleSearchEnter();
+      handleSearchItemSelected();
       break;
   }
 });
 
-searchInput.addEventListener('input', async (ev) => {
-  const text = ev.target.value;
+function handleSearchCursorUpDown(isDownwards) {
+  const selectedResult = document.querySelector(`#${resultsElmntId} .selected`);
 
-  if (!text) {
-    const sr = document.getElementById(srId);
-    sr.removeAttribute('state');
-    sr.replaceWith(sr.cloneNode(false));
-    return;
+  if (selectedResult) {
+    selectedResult.classList.remove('selected');
+    selectedResult = isDownwards ? selectedResult.nextSibling : selectedResult.previousSibling;
+  } else {
+    selectedResult = isDownwards ? resultsContainer.firstChild : resultsContainer.lastChild;
   }
 
-  document.getElementById(srId).setAttribute('state', 'loading');
+  selectedResult && selectedResult.classList.add('selected');
+}
+
+function handleSearchItemSelected() {
+  const selectedResult = document.querySelector(`#${resultsElmntId} .selected`)
+  selectedResult.click();
+}
+
+
+
+// Simple filtering by *attributes* and *kind* per declaration
+// -------------------------
+
+/* Get all elements for filtering */
+const filtersToggleButton = document.getElementById('search_filters_btn');
+const filtersContainer = document.getElementById('filters_container');
+const filtersForm = document.getElementById('filters_form');
+const closeFiltersBtn = document.getElementById('close_filters_btn');
+
+/* Handle opening/closing filters container */
+function closeFiltersDisplay() {
+  filtersContainer.style.display = 'none';
+}
+closeFiltersBtn.addEventListener("click", closeFiltersDisplay);
 
-  const result = await declSearch(text);
-  if (ev.target.value != text) return;
+function openFiltersDisplay() {
+  filtersContainer.style.display = 'block';
+}
 
-  const oldSR = document.getElementById('search_results');
-  const sr = oldSR.cloneNode(false);
-  for (const {decl} of result) {
-    const d = sr.appendChild(document.createElement('a'));
-    d.innerText = decl;
-    d.title = decl;
-    d.href = `${siteRoot}find/${decl}`;
+function toggleFiltersDisplay() {
+  const filtersContainerStyle = (!filtersContainer.style.display || filtersContainer.style.display.length === 0) ?
+    getComputedStyle(filtersContainer).display : 
+    filtersContainer.style.display;
+  const isOpen = filtersContainerStyle !== 'none';
+  if (isOpen) {
+    closeFiltersDisplay();
+  } else {
+    openFiltersDisplay();
   }
-  sr.setAttribute('state', 'done');
-  oldSR.replaceWith(sr);
-});
+}
+filtersToggleButton.addEventListener("click", toggleFiltersDisplay);
+
+/* Handle submit chosen filters */
+const submitFiltersFormHandler = (ev) => {
+  ev.preventDefault();
+  const attributeBoxNodes = filtersForm.querySelectorAll('input[name=attribute]:checked');
+  const kindBoxNodes = filtersForm.querySelectorAll('input[name=kind]:checked');
 
+  
+  filters.attributes = [];
+  attributeBoxNodes?.forEach(e => filters.attributes.push(e.value));
 
+  filters.kind = [];
+  kindBoxNodes?.forEach(e => filters.kind.push(e.value));
+
+  closeFiltersDisplay();
+  submitSearchFormHandler(ev);
+};
+filtersForm.addEventListener('submit', submitFiltersFormHandler);
 
 
 
 
 // 404 page goodies
 // ----------------
+const suggestionsElmnt = document.getElementById('howabout');
+if (suggestionsElmnt) {
+  suggestionsElmnt.innerText = "Please wait a second.  I'll try to help you.";
 
-const howabout = document.getElementById('howabout');
-if (howabout) {
-  howabout.innerText = "Please wait a second.  I'll try to help you.";
-
-  howabout.parentNode
-      .insertBefore(document.createElement('pre'), howabout)
-      .appendChild(document.createElement('code'))
-      .innerText = window.location.href.replace(/[/]/g, '/\u200b');
+  suggestionsElmnt.parentNode
+    .insertBefore(document.createElement('pre'), suggestionsElmnt)
+    .appendChild(document.createElement('code'))
+    .innerText = window.location.href.replace(/[/]/g, '/\u200b');
 
   const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1];
-  declSearch(query).then((results) => {
-      howabout.innerText = 'How about one of these instead:';
-      const ul = howabout.appendChild(document.createElement('ul'));
-      for (const {decl} of results) {
-          const li = ul.appendChild(document.createElement('li'));
-          const a = li.appendChild(document.createElement('a'));
-          a.href = `${siteRoot}find/${decl}`;
-          a.appendChild(document.createElement('code')).innerText = decl;
-      }
+  searchIndexedData(query).then((results) => {
+    suggestionsElmnt.innerText = 'How about one of these instead:';
+    const ul = suggestionsElmnt.appendChild(document.createElement('ul'));
+    for (const { decl } of results) {
+      const li = ul.appendChild(document.createElement('li'));
+      const a = li.appendChild(document.createElement('a'));
+      a.href = `${siteRoot}find/${decl}`;
+      a.appendChild(document.createElement('code')).innerText = decl;
+    }
   });
 }
 
diff --git a/print_docs.py b/print_docs.py
index 2584b29..2cc252d 100644
--- a/print_docs.py
+++ b/print_docs.py
@@ -713,9 +713,9 @@ def mk_export_map_entry(decl_name, filename, kind, is_meta, line, args, tp):
           'src_link': library_link(filename, line),
           'docs_link': f'{site_root}{filename.url}#{decl_name}'}
 
-def mk_export_db(loc_map, file_map):
+def mk_export_db(file_map):
   export_db = {}
-  for fn, decls in file_map.items():
+  for _, decls in file_map.items():
     for obj in decls:
       export_db[obj['name']] = mk_export_map_entry(obj['name'], obj['filename'], obj['kind'], obj['is_meta'], obj['line'], obj['args'], obj['type'])
       export_db[obj['name']]['decl_header_html'] = env.get_template('decl_header.j2').render(decl=obj)
@@ -730,6 +730,44 @@ def write_export_db(export_db):
   with gzip.GzipFile(html_root + 'export_db.json.gz', 'w') as zout:
     zout.write(json_str.encode('utf-8'))
 
+def mk_export_searchable_map_entry(filename_name, name, description, kind = '', attributes = []):
+  return {
+    'module': filename_name,
+    'name': name,
+    'description': description,
+    'kind': kind,
+    'attributes': attributes,
+  }
+
+def mk_export_searchable_db(file_map, tactic_docs):
+  export_searchable_db = []
+
+  for fn, decls in file_map.items():
+    filename_name = str(fn.url)
+    for obj in decls:
+      decl_entry = mk_export_searchable_map_entry(filename_name, obj['name'], obj['doc_string'], obj['kind'], obj['attributes'])
+      export_searchable_db.append(decl_entry)
+      for (cstr_name, _) in obj['constructors']:
+        cstr_entry = mk_export_searchable_map_entry(filename_name, cstr_name, obj['doc_string'], obj['kind'], obj['attributes'])
+        export_searchable_db.append(cstr_entry)
+      for (sf_name, _) in obj['structure_fields']:
+        sf_entry = mk_export_searchable_map_entry(filename_name, sf_name, obj['doc_string'], obj['kind'], obj['attributes'])
+        export_searchable_db.append(sf_entry)
+
+  for tactic in tactic_docs:
+    # category is the singular form of each docs webpage in 'General documentation'
+    # e.g. 'tactic' -> 'tactics.html'
+    tactic_entry_container_name = f"{tactic['category']}s.html"
+    tactic_entry = mk_export_searchable_map_entry(tactic_entry_container_name, tactic['name'], tactic['description'])
+    export_searchable_db.append(tactic_entry)
+
+  return export_searchable_db
+
+def write_export_searchable_db(searchable_data):
+  json_str = json.dumps(searchable_data)
+  with open_outfile('searchable_data.bmp') as out:
+    out.write(json_str)
+
 def main():
   bib = parse_bib_file(f'{local_lean_root}docs/references.bib')
   file_map, loc_map, notes, mod_docs, instances, tactic_docs = load_json()
@@ -740,7 +778,8 @@ def main():
   copy_css_and_js(html_root, use_symlinks=cl_args.l)
   copy_yaml_bib_files(html_root)
   copy_static_files(html_root)
-  write_export_db(mk_export_db(loc_map, file_map))
+  write_export_db(mk_export_db(file_map))
+  write_export_searchable_db(mk_export_searchable_db(file_map, tactic_docs))
   write_site_map(file_map)
 
 if __name__ == '__main__':
diff --git a/searchWorker.js b/searchWorker.js
index 6fadb54..2508066 100644
--- a/searchWorker.js
+++ b/searchWorker.js
@@ -1,27 +1,71 @@
+// Access indexed data structure to be used for searching through the documentation
 const req = new XMLHttpRequest();
-req.open('GET', 'decl.bmp', false /* blocking */);
-req.responseType = 'text';
-req.send();
-
-const declNames = req.responseText.split('\n');
 
-// Adapted from the default tokenizer and
-// https://util.unicode.org/UnicodeJsps/list-unicodeset.jsp?a=%5Cp%7BZ%7D&abb=on&c=on&esc=on&g=&i=
-const SEPARATOR = /[._\n\r \u00A0\u1680\u2000-\u200A\u2028\u2029\u202F\u205F\u3000]+/u
+req.open('GET', 'searchable_data.bmp', false /* blocking */);
+req.responseType = 'json';
+req.send();
 
 importScripts('https://cdn.jsdelivr.net/npm/minisearch@2.4.1/dist/umd/index.min.js');
+    // Include options as per API specs: https://lucaong.github.io/minisearch/modules/_minisearch_.html
 const miniSearch = new MiniSearch({
-    fields: ['decl'],
-    storeFields: ['decl'],
-    tokenize: text => text.split(SEPARATOR),
+    idField: 'name',
+    fields: ['module', 'name', 'description'],
+    storeFields: ['module', 'name', 'description', 'attributes', 'kind']
 });
-miniSearch.addAll(declNames.map((decl, id) => ({decl, id})));
+
+const indexedData = req.response;
+miniSearch.addAll(indexedData);
 
 onconnect = ({ports: [port]}) =>
-    port.onmessage = ({data}) => {
-        const results = miniSearch.search(data.q, {
-            prefix: (term) => term.length > 3,
-            fuzzy: (term) => term.length > 3 && 0.2,
+port.onmessage = ({ data }) => {
+    const { query, filters, maxCount } = data;
+    const filterFunc = (result) => filterItemResult(result, filters);
+    const sanitizedQuery = query.trim();
+    if (sanitizedQuery && typeof sanitizedQuery === "string" && sanitizedQuery.length > 0) {
+        const results = miniSearch.search(sanitizedQuery, {
+            boost: { module: 1, description: 2, name: 3 },
+            combineWith: 'AND',
+            filter: filterFunc,
+            // prefix: (term) => term.length > 3,
+            // fuzzy: (term) => term.length > 3 && 0.2,
         });
-        port.postMessage(results.slice(0, 20));
-    };
+        
+        const response = typeof maxCount === "number" && maxCount >= 0 ? results.slice(0, maxCount) : results;
+        console.log(response)
+        port.postMessage({response, total: results.length});
+    }
+    port.postMessage({response: [], total: 0});
+};
+
+const filterItemResult = (result, filters = {}) => {
+    const { attributes: attrFilter, kind: kindFilter } = filters;
+    const hasAttrFilter = attrFilter && attrFilter.length > 0;
+    const hasKindFilter = kindFilter && kindFilter.length > 0;
+
+    if (!hasAttrFilter && !hasKindFilter) {
+        return true;
+    }
+    
+    const { attributes: attrRes, kind: kindRes } = result;
+    let isResultAttrIncluded = false;
+    let isResultKindIncluded = false;
+
+    if (hasKindFilter) {
+        isResultKindIncluded = kindFilter.includes(kindRes);
+    }
+
+    if (hasAttrFilter) {
+        for (let attribute of attrRes) {
+            if (attrFilter.includes(attribute)) {
+                isResultAttrIncluded = true;
+                break;
+            }
+        }
+    } 
+
+    return hasKindFilter && hasAttrFilter ? 
+        (isResultAttrIncluded && isResultKindIncluded) : 
+        hasAttrFilter ? 
+            isResultAttrIncluded : 
+            isResultKindIncluded;
+}
diff --git a/style.css b/style.css
index 5743e2f..ebd1806 100644
--- a/style.css
+++ b/style.css
@@ -114,8 +114,7 @@ header {
 @media screen and (max-width: 700px) {
     header h1 span { display: none; }
     :root { --header-side-padding: 1ex; }
-    #search_form button { display: none; }
-    #search_form input { width: 100%; }
+    #search_form input { width: 60%; }
     header #search_results {
         left: 1ex;
         right: 1ex;
@@ -145,63 +144,6 @@ header header_filename {
     }
 }
 
-/* inserted by nav.js */
-#search_results {
-    position: absolute;
-    top: var(--header-height);
-    right: calc(var(--header-side-padding));
-    width: calc(20em + 4em);
-    z-index: 1;
-    background: var(--header-bg);
-    border: 1px solid #aaa;
-    border-top: none;
-    overflow-x: hidden;
-    overflow-y: auto;
-    max-height: calc(100vh - var(--header-height));
-}
-
-#search_results:empty {
-    display: none;
-}
-
-#search_results[state="loading"]:empty {
-    display: block;
-    cursor: progress;
-}
-#search_results[state="loading"]:empty::before {
-    display: block;
-    content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 ';
-    padding: 1ex;
-    animation: marquee 10s linear infinite;
-}
-@keyframes marquee {
-    0% { transform: translate(100%, 0); }
-    100% { transform: translate(-100%, 0); }
-}
-
-#search_results[state="done"]:empty {
-    display: block;
-    text-align: center;
-    padding: 1ex;
-}
-#search_results[state="done"]:empty::before {
-    content: '(no results)';
-    font-style: italic;
-}
-
-#search_results a {
-    display: block;
-    color: inherit;
-    padding: 1ex;
-    border-left: 0.5ex solid transparent;
-    padding-left: 0.5ex;
-    cursor: pointer;
-}
-#search_results .selected {
-    background: white;
-    border-color: #f0a202;
-}
-
 main, nav {
     margin-top: calc(var(--header-height) + 1em);
 }
@@ -560,3 +502,126 @@ a:hover {
     margin-top: 2em;
     margin-bottom: 2em;
 }
+
+
+/* Form for filtering search through declarations */
+#filters_container {
+    display: none;
+    width: 300px;
+    height: 250px;
+    position: absolute;
+    right: calc(var(--header-side-padding));
+    top: var(--header-height);
+    background: var(--header-bg);
+    border: 1px solid rgb(218, 216, 216);
+    border-top: none;
+    overflow-y: auto;
+    overflow-x: hidden;
+    z-index: 2;
+}
+
+#filters_container #filters_display {
+    display: flex;
+	flex-wrap: wrap;
+	justify-content: space-around;
+    margin-top: 16px;
+    margin-bottom: 16px;
+}
+
+/* Style the close button (span) */
+#filters_container #close_filters_btn,
+#search_results #close_results_btn  {
+    cursor: pointer;
+    position: absolute;
+    top: 5px;
+    right: 0%;
+    padding: 0 8px 0 8px;
+    margin: 8px;
+    transform: translate(0%, -50%);
+  }
+  
+#filters_container #close_filters_btn:hover {background: #bbb;}
+#search_results #close_results_btn:hover {background: #bbb;}
+
+#filters_container #submit_filters_btn {
+    position: relative;
+    left: 35%;
+}
+/* Form for searching through declarations */
+#search_results {
+    display: none;
+    position: absolute;
+    top: var(--header-height);
+    right: calc(var(--header-side-padding));
+    width: 380px;
+    z-index: 1;
+    background: var(--header-bg);
+    border: 1px solid #aaa;
+    border-top: none;
+    overflow-x: auto;
+    overflow-y: auto;
+    max-height: calc(60vh - var(--header-height));
+}
+
+#search_results.condensed {
+    width: 380px;
+    max-height: calc(60vh - var(--header-height));
+}
+
+#search_results.full_width {
+    width: 1080px;
+    max-height: calc(95vh - var(--header-height));
+    border: 1px solid #aaa;
+    box-shadow: 5px 3px 0.8em #60a0b0, -0.5em 0 0.8em #60a0b0;
+}
+
+#search_results:empty {
+    display: none;
+}
+
+#search_results[state="loading"]:empty {
+    display: block;
+    cursor: progress;
+}
+#search_results[state="loading"]:empty::before {
+    display: block;
+    content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 ';
+    padding: 1ex;
+    animation: marquee 10s linear infinite;
+}
+@keyframes marquee {
+    0% { transform: translate(100%, 0); }
+    100% { transform: translate(-100%, 0); }
+}
+
+#search-results #search_info {
+    font-size: 50%;
+}
+
+#search_results .search_result_item a {
+    display: block;
+    color: inherit;
+    padding: 4px;
+    border-top: 1px dashed #70a0d0;
+    cursor: pointer;
+}
+#search_results .search_result_item a .result_module {
+    font-size: 0.7em;
+    margin-top: 1px;
+}
+#search_results .search_result_item a .result_comment {
+    font-size: 0.8em;
+    margin-top: -0.5em;
+    font-family: 'Open Sans', sans-serif;
+}
+
+#search_results .selected {
+    background: white;
+    border-color: #f0a202;
+}
+
+.link_coloring {
+    color: hsl(210, 100%, 30%);
+    text-decoration: none;
+    cursor: pointer;
+}
\ No newline at end of file
diff --git a/templates/base.j2 b/templates/base.j2
index 129c625..83d4cc2 100644
--- a/templates/base.j2
+++ b/templates/base.j2
@@ -28,11 +28,106 @@
     <h1><label for="nav_toggle"></label><a href="https://leanprover-community.github.io">mathlib</a>
         <span>documentation</span></h1>
     <p class="header_filename break_within">{% block doctitle %}{{ self.title() }}{% endblock %}</p>
-    <form action="https://google.com/search" method="get" id="search_form">
+    <form id="search_form">
         <input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs">
-        <input type="text" name="q" autocomplete="off">
-        <button>Google site search</button>
+        <input type="text" name="query" autocomplete="off">
+        <button type="button" id="search_filters_btn">Filter</button>
+        <button type="submit">Search</button>
+        <div id="search_results"></div>
     </form>
+    <div id="filters_container">
+        <span class="close" id="close_filters_btn">x</span>
+        <form id="filters_form">
+            <div id="filters_display">
+                <div id="attributes_filter">
+                    Attributes:
+                    <br>
+                    <input type="checkbox" 
+                    name="attribute"
+                    value="simp"
+                    id="simp"
+                    >
+                    <label for="simp">simp</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="attribute"
+                    value="nolint"
+                    id="nolint"
+                    >
+                    <label for="nolint">nolint</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="attribute"
+                    value="ext"
+                    id="ext"
+                    >
+                    <label for="ext">ext</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="attribute"
+                    value="instance"
+                    id="instance"
+                    >
+                    <label for="instance">instance</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="attribute"
+                    value="class"
+                    id="class"
+                    >
+                    <label for="class">class</label>
+                    <br>
+                </div>
+                <div id="kinds_filter">
+                    Kind:
+                    <br>
+                    <input type="checkbox" 
+                    name="kind"
+                    value="structure"
+                    id="structure"
+                    >
+                    <label for="structure">structure</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="kind"
+                    value="theorem"
+                    id="theorem"
+                    >
+                    <label for="theorem">theorem</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="kind"
+                    value="def"
+                    id="def"
+                    >
+                    <label for="def">definition</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="kind"
+                    value="constant"
+                    id="constant"
+                    >
+                    <label for="constant">constant</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="kind"
+                    value="axiom"
+                    id="axiom"
+                    >
+                    <label for="axiom">axiom</label>
+                    <br>
+                    <input type="checkbox" 
+                    name="kind"
+                    value="inductive"
+                    id="inductive"
+                    >
+                    <label for="inductive">inductive</label>
+                    <br>
+                </div>
+            </div>   
+            <button type="submit" id="submit_filters_btn">Submit filters</button>
+        </form>
+    </div>
 </header>
 
 <nav class="internal_nav">{% block internal_nav %}{% endblock %}</nav>