I hereby claim:
- I am ayberkt on github.
- I am ayberkt (https://keybase.io/ayberkt) on keybase.
- I have a public key whose fingerprint is 17AA 88FB 333F F93A 4C3A 2531 2409 CCD7 6D12 4F2B
To claim this, I am signing this object:
{-# OPTIONS --cubical --safe #-} | |
module Problem where | |
open import Cubical.Core.Everything using ( _≡_ | |
; Type | |
; Σ | |
; Σ-syntax | |
; _,_ ) | |
open import Cubical.Data.Prod using ( _,_; proj₁; proj₂ ) |
I hereby claim:
To claim this, I am signing this object:
I hereby claim:
To claim this, I am signing this object:
ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQDB/ThJZfpaHI337U5cq56ydyg8PuoYUYfxgRkbHTIq24JLO49x6YxsyaFL2cqHZwmzLMuMQrGtOlznnc+Ud88ni6nfgHX1zztNNFZ6EzUXsEKIXqqmuQEGXWg1pLuMMRjB6qaG781K3Lrd3yjmXA8+f5/+3aLAv85cy+tVeZsF8dyAhyBq75wLj1E2kNfBcqBbZkGek4UgzSL/9MqgtTQp9vWAPpR+d8RznIf79iZo0sPmNyW0nOzPFJiMbOcbN8fEChPQv3xGM7AWzdCxY+hGlnqk/Ki3b4+7rmZ5a+j+NqLogmMABeSwwdmDzWRvUKt/yzsZ9KNAfJqZTCTfChNd tosun2@illinois.edu |
concrete CityTur of City = open Prelude in { | |
flags | |
lexer=bind; | |
param | |
WowelType = Front | Back; | |
DefAccCase = OnlyI WowelType | SoftenCons WowelType | InsertY WowelType; | |
lincat | |
Phrase = Str; |
structure Regex = | |
struct | |
datatype regexp = | |
Zero | |
| One | |
| Char of char | |
| Times of regexp * regexp | |
| Plus of regexp * regexp | |
| Star of regexp |
(define-fun is-prob ((r Real)) Bool (and (>= r 0) (<= r 1))) | |
(define-fun equi ((a Real) (b Real) (c Real) (d Real) (r Real) (s Real)) Real | |
(+ (* r s a) (* r (- 1 s) b) (* (- 1 r) s c) (* (- 1 r) (- 1 s) d))) | |
(assert | |
(forall ((x1 Real) (y1 Real) (w1 Real) (z1 Real) | |
(x2 Real) (y2 Real) (w2 Real) (z2 Real)) | |
(exists ((r Real) (s Real)) | |
(=> |
all: | |
pdflatex paper.tex | |
bib: | |
latex paper.tex && bibtex paper.aux && latex paper.tex && pdflatex paper.tex | |
clean: | |
rm -f paper.pdf | |
rm -f paper.aux | |
rm -f paper.log |