hacklex

module FStar.Algebra.Classes.Equatable
 
module TC = FStar.Tactics.Typeclasses

class equatable (t:Type) = {
  eq: t -> t -> bool;
  reflexivity : (x:t -> Lemma (eq x x));
  symmetry: (x:t -> y:t -> Lemma (requires eq x y) 
                               (ensures eq y x));
  transitivity: (x:t -> y:t -> z:t -> Lemma (requires eq x y /\ eq y z) 

hacklex

module Sandbox

open FStar.Seq

let under (x: nat) = z:nat{z<x}

let index_for #t (x:seq t) = under (length x)

let rec select_by_key (#key_type: eqtype) 
                      (#value_type: Type) 

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"]

hacklex

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

namespace Avalonia.Data.Converters;

public class ColorConverter : IValueConverter
{  

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

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

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 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 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
 
// 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