jakobrs

import Mathlib.Data.Multiset.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.Group.Nat.Defs
import Mathlib.Data.Multiset.MapFold

inductive Wff
  | var (name : String)
  | imp (a b : Wff)
  | not (a : Wff)
  | or (a b : Wff)

jakobrs

def List.instMonad : Monad List where
  pure x := [x]
  bind := List.flatMap

def List.guard : Bool -> List Unit
  | false => []
  | true => [()]

declare_syntax_cat comprRule

jakobrs

IO
Id
id
Div
EIO
Fin
Fix
Iff
Inf
Int

jakobrs

#include <functional>
#include <iostream>
#include <memory>
#include <optional>
#include <variant>

template <typename T> struct Thunk {
  std::variant<T, std::function<T()>> contents;

  Thunk(const T &val) : contents{val} {}

jakobrs

#include <lean/lean.h>

#include <cstring>
#include <fcntl.h>
#include <linux/if.h>
#include <linux/if_tun.h>
#include <string>
#include <sys/ioctl.h>
#include <unistd.h>

jakobrs

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoFieldSelectors #-}

import Data.Function ((&))
import Data.Functor.Identity (Identity (..))
import Data.Monoid (Endo (..), Sum (..))

jakobrs

{-# LANGUAGE ViewPatterns #-}

import Control.Monad (forM_)
import Control.Monad.ST (ST)
import Data.Functor ((<&>))
import Data.Monoid (Endo (..))
import Data.STRef (STRef, newSTRef)
import Data.Vector qualified as V
import Data.Vector.Generic.Mutable qualified as GV
import Data.Vector.Mutable qualified as MV

jakobrs

import Data.Ratio

-- Q5 = Q(sqrt(5))
data Q5 = Q5 Rational Rational deriving (Show, Eq)

instance Num Q5 where
  fromInteger n = Q5 (fromInteger n) 0
  Q5 a b + Q5 c d = Q5 (a + c) (b + d)
  Q5 a b * Q5 c d = Q5 (a * c + 5 * b * d) (a * d + b * c)
  negate (Q5 a b) = Q5 (-a) (-b)

jakobrs

// #define USE_BITS_STDCPP
// #define USE_RARE_HEADERS

#ifdef USE_BITS_STDCPP
#include <bits/stdc++.h>
#endif

#include <algorithm>
#include <array>
#include <iostream>

jakobrs

#include "veb.hpp"
#include <iostream>

int main() {
  std::cin.tie(nullptr)->sync_with_stdio(false);

  assert((1 << 18 > 200'001));

  int q;
  std::cin >> q;