Brian Milnes

Amos Robinson wants to put in a let that won't unfold but did not know how to build. Liking a clean build, I tried it for the first time on...

The functional versions of x_intro/elim are used about twice as much as the introduce/eliminate sugar. And if you are generating propositions via functions, and the more serious projects do, you...

Automatically print full names when types don't match but have the same short name

1

The attached file shows this bug on the last definition (which was under construction), print_implicits/universes was on but provided no help. (Error 19) Subtyping check failed; expected type p’: pfp...

Folks, A Seq length = n constraint in a conjunctive refinement type is order dependent. (* This demonstrates a type checking problem in which a sequence is used before it's...

type listset' (e: eqtype) = list e let rec lsmem #e (e': e) (ls: listset' e) : Tot bool = match ls with | [] -> false | hd::tl ->...

module DoubleVarRefineError let no_error (p : list int{Cons? p}) (p' : list int{Cons? p'}) = 0 /// Unbound variables let error1 (p p': list int{Cons? p}) = 0 let error2...

I just missed using a variable (let s' = ... s ... in ... s ..., instead of s'). And my routine proved its bounds checks, but if I had...

Refining ADT types in record.

2

Looks like I can't refine ADT types in record definitions. ```f* module RecordRefinement type aType = | B : string -> aType | C : string -> aType type aTypeB...

module LiteralStringRefBug open FStar.String let replacePrefix (pre: string) (s: string{length pre

I was writing some test code. Yes, I know you all probably think its a bit passe, but it helps while learning to see that my specifications are what I...