hacklex

module FStar.Algebra.Setoid

module TC = FStar.Tactics.Typeclasses
module F = FStar.FunctionalExtensionality


open FStar.Tactics

class equivalence_relation a = {
  eq : a -> a -> bool;

hacklex

module Sandbox


open FStar.Seq
open FStar.IntegerIntervals

let rec subseq_from_indices (#n: nat) (s: seq nat {length s == n})
                                    (h: seq (under n))
  : Tot (seq nat) (decreases length h) = 
  if length h = 0 then empty

hacklex

module Sandbox
 
// no complications or wasted verification time is permitted below this line.
#set-options "--ifuel 0 --fuel 0 --z3rlimit 1"

type binary_op (a:Type) = a -> a -> a
type unary_op (a:Type) = a -> a
type predicate (a:Type) = a -> bool
type binary_relation (a: Type) = a -> a -> bool
 

hacklex

module Sandbox

open FStar
open LowStar.Buffer
open LowStar.BufferOps
open FStar.HyperStack.ST

module Buffer = LowStar.Buffer

unfold let test_pre (b r: buffer UInt32.t) (h: FStar.HyperStack.mem): Type0 =

hacklex

module Sandbox

#set-options "--ifuel 0 --fuel 0 --z3rlimit 1"

type unat = 
  | Z : unat
  | S : (prev: unat) -> unat
   
#set-options "--ifuel 1 --fuel 0"
let rec unat_to_nat (x: unat) : nat = 

hacklex

module PigeonPrinciple
 
open FStar.IntegerIntervals 

open FStar.Seq
  
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

hacklex

module FStarFreeze

let unbounded (f: nat -> int) = forall (m: nat). exists (n:nat). abs (f n) > m
assume val f : (z:(nat -> int){unbounded z})

let g : (nat -> int) = fun x -> f (x+1)
 
let find_above_for_g (m:nat) : Lemma(exists (i:nat). abs(g i) > m) = 
  assert (unbounded f); // apply forall to m
  eliminate exists (n:nat). abs(f n) > m

hacklex

public class PhoneWaveCollectionChangeAggregator<T> : TransactionChange
{
    List<(bool isRemove, int index, T item)> _changes = new();
     
    ObservableCollection<T> _target;

    public PhoneWaveCollectionChangeAggregator(ObservableCollection<T> target)
    { 
        _target = target;

hacklex

using System;
using System.Globalization;
using Avalonia;
using Avalonia.Data;
using Avalonia.Media;  

namespace Avalonia.Data.Converters;

public class ColorConverter : IValueConverter
{  

hacklex

module Sandbox

type binary_op (a:Type) = a -> a -> a
type unary_op (a:Type) = a -> a
type predicate (a:Type) = a -> bool
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
[@@"opaque_to_smt"]