jittat

-- Mostly taken from Xena project at 
-- https://github.com/ImperialCollegeLondon/M40001_lean/blob/master/src/2021/logic/README.md

import tactic -- imports all the Lean tactics

variables (P Q R W S: Prop)

/-
## Tactics:

jittat

Keybase proof

I hereby claim:

• I am jittat on github.
• I am jittat (https://keybase.io/jittat) on keybase.
• I have a public key ASB3KKWyANrRfJTIv5KCGWeqAn3f71jxzvLuDyyi5f57uAo

To claim this, I am signing this object:

jittat

jittat

class Box:
    def __init__(self,r,c,board):
        self.r = r
        self.c = c
        self.board = board

class Player:
    def __init__(self,r,c,board):
        self.r = r
        self.c = c

jittat

class Box:
    def __init__(self,r,c,board):
        self.r = r
        self.c = c
        self.board = board

class Player:
    def __init__(self,r,c,board):
        self.r = r
        self.c = c

jittat

class Box:
    def __init__(self,r,c,board):
        pass

class Player:
    def __init__(self,r,c,board):
        pass

    def move_up(self):
        pass

jittat

jittat

def extract_line(line):
    """
    >>> extract_line("* hello world")
    ('hello world', 1)
    >>> extract_line("** this  is a ** test!!")
    ('this  is a ** test!!', 2)
    """
    depth = 0
    l = len(line)
    while (depth < l) and (line[depth] == '*'):

jittat

import sys
import getpass
import requests
import codecs
from bs4 import BeautifulSoup

CAMPUS = 'B'

def login(username, password):
    logindata = { 'UserName': username,

jittat

def to_roman(a):
    if a >= '๐' and a <= '๙':
        return chr(ord(a) - ord('๐') + ord('0'))
    return a

def is_same_digit(a,b):
    if a < '0' and a > '9':
        return False

    aa = to_roman(a)