paulzfm

trait Bug {

  trait A {
    def foo(implicit f: Unit => Unit): A = ??? // fix 1: remove `= ???`

    def bar(implicit f: Unit => Unit): A
  }

  def baz(f: Int => A): Boolean = ??? // fix 2: rename this `baz` to another (such as `baz2`)

paulzfm

#lang rosette

(require rosette/query/debug rosette/lib/render rosette/lib/synthax)

; A macro to create an automaton.
(define-syntax automaton
  (syntax-rules (: →)  
    [(_ init-state
        (state : (label → target) ...) ...)
     (letrec ([state

paulzfm

(**-- Simply Typed Lambda-Calculus Boolean Extensions --**)

(* ################################################################# *)
(** * Auxilaries *)

Set Warnings "-notation-overridden,-parsing".

Require Import Coq.Bool.Bool.
Require Import Coq.Strings.String.
Require Import Coq.Logic.FunctionalExtensionality.

paulzfm

(define-sort Bit8 () (_ BitVec 8)) ; 8-bit vector
(declare-const hP Int) 		; choices for operators: plus, mul, shl, shr
(declare-const hE1 Bool)	; choices for E1: true for x, false for C
(declare-const hE2 Bool)	; choices for E2: true for x, false for C
(declare-const c1 Bit8)		; choices for C1: 0~0b11111111
(declare-const c2 Bit8) 	; choices for C2: 0~0b11111111
(assert (and (>= hP 0) (< hP 4))) ; 0=plus, 1=mul, 2=shl, 3=shr
; Definition of P(x)
(define-fun prog ((x Bit8)) Bit8
    (let ((left (ite hE1 c1 x))

paulzfm

\setCJKmainfont[BoldFont=SimHei,ItalicFont=KaiTi]{SimSun}
\setCJKsansfont{SimHei}
\setCJKmonofont{KaiTi}
\setCJKfamilyfont{zhsong}{SimSun}
\setCJKfamilyfont{zhhei}{SimHei}
\setCJKfamilyfont{zhfs}{FangSong}
\setCJKfamilyfont{zhkai}{KaiTi}
\NewDocumentCommand\songti{}{\CJKfamily{zhsong}}
\NewDocumentCommand\heiti{}{\CJKfamily{zhhei}}
\NewDocumentCommand\fangsong{}{\CJKfamily{zhfs}}