FStar

FStar copied to clipboard

Fix typos and exercise file in part 1 of book

1

Not sure if there is a better way to edit the code for `twice`, where an implementation is given and readers are expected to fill in a missing type declaration.

SwampertX

Typeclass resolution don't work with typeclass that depend on others

2

See the following example: ```fstar class tc1 (a:Type) = { tc1_method: unit; } class tc2 (a:Type) {|tc1 a|} (b:Type)= { //This function use the methods of tc1 to do its...

TWal

Type inference works in "normal mode" but fails in lax mode (hence in dependency loading)

3

See the following example A.fst: ```fstar module A assume val bytes_like: Type0 -> Type0 assume val parser_serializer: bytes:Type0 -> pf:bytes_like bytes -> Type0 -> Type0 assume val bind: #bytes:Type0 ->...

TWal

This unusual way of writing a dependent pair: ``` module TT let test (a: Type) (b: (a → Type)) (y: (v: a) & b v) = () ``` is accepted...

nikswamy

See the following example, happening in a context similar to #2478 . ```fstar assume val bytes_like: Type0 -> Type0 assume val parser_serializer: Type0 -> Type0 type key (bytes:Type0) (pf:bytes_like bytes)...

TWal

`unfold` don't work as expected in binder attributes

1

See the following example: ```fstar module UnfoldAttr open FStar.Tactics irreducible let attrib (#a:Type) (x:a) = () unfold let string_attrib (s:string) = attrib ("[" ^ s ^ "]") type test =...

TWal

This issue is for the behavior noted in #2558. Nik mentioned this looks like a bug rather than expected behavior. I saw some unexpected behavior in what was normalized using...

klinvill

See the code below: ```fstar let test_annot (#a:Type0) (x:int) = () type test_type = { [@@@ test_annot 1337] x: int; } ``` It gives the following error: ``` ASSERTION FAILURE:...

TWal

Installation through opam always crashes at `Steel.ST.Array.Util.fst`?

1

I cannot get opam to build dev version of fstar (`2022.04.23` this time, but it was failing for a few months now), the build process always crashes at `Steel.ST.Array.Util.fst` (surprisingly,...

LukeXuan

Create file ``` module AlgebraTypes type binary_relation (a: Type) = a -> a -> bool [@@"opaque_to_smt"] let is_reflexive (#a:Type) (r: binary_relation a) = forall (x:a). x `r` x ``` Hover...

kant2002