Based on Huet 1976, §5.7.2
From earlier sections
V
is a countably infinite set of variables.C
a finite set of constructors.a : C -> Nat
an arity function.R : V -/-> Typ
a partial environment function.
/// BigVector is an arbitrary sized vector-like data structure, | |
/// implemented using an on-chain B+ Tree. | |
/// | |
/// Elements in the vector are distributed between a fixed size | |
/// `tail`, stored in a `vector`, and an arbitrary size B+ Tree for | |
/// the rest of the data. Nodes in the B+ Tree are stored as | |
/// individual dynamic fields hanging off the `BigVector`. | |
/// | |
/// This data structure supports: | |
/// |
[package] | |
name = "fermat-bench" | |
version = "0.1.0" | |
edition = "2021" | |
[dev-dependencies] | |
criterion = "0.5" | |
[[bench]] | |
name = "bench" |
[package] | |
name = "Table Test" | |
version = "0.1.0" | |
[dependencies] | |
Sui = { ... } | |
[addresses] | |
std = "0x1" | |
sui = "0x2" |
module p::example { | |
use sui::coin::{Self, Coin}; | |
use sui::dynamic_field as field; | |
use sui::object::UID; | |
use sui::tx_context::TxContext; | |
struct Manager has key { id: UID, /* ... */ } | |
struct Label<phantom COIN> has copy, drop, store {} | |
entry fun handle_coin<COIN>(m: &mut Manager, coin: Coin<COIN>, ctx: &mut TxContext) { |
--- | |
compiled_package_info: | |
package_name: example | |
address_alias_instantiation: | |
example: "0000000000000000000000000000000000000000" | |
std: "0000000000000000000000000000000000000001" | |
sui: "0000000000000000000000000000000000000002" | |
source_digest: E221B8FCD48A736A2DF75C6E39E806D621BE87E68D4049A99153D5986E77112A | |
build_flags: | |
dev_mode: false |
module RBTree where | |
open import Agda.Primitive public | |
using (Level; lzero; lsuc; _⊔_) | |
data Σ {l k} (A : Set l) (B : A → Set k) : Set (l ⊔ k) where | |
_,_ : (a : A) → (b : B a) → Σ A B | |
infixr 10 _,_ | |
fst : ∀ {l k} {A : Set l} {B : A → Set k} -> Σ A B -> A |
module HList where | |
open import Agda.Primitive public | |
using (Level; lzero; lsuc; _⊔_) | |
data Σ {l k} (A : Set l) (B : A -> Set k) : Set (l ⊔ k) where | |
_,_ : (a : A) -> (B a) -> Σ A B | |
infixr 3 _,_ |
module Fact where | |
fact :: Integer -> Integer | |
fact 0 = 1 | |
fact n = n * fact (n-1) | |
factk :: Integer -> (Integer -> r) -> r | |
factk 0 k = k 1 | |
factk n k = factk (n-1) (k . (n*)) |
Based on Huet 1976, §5.7.2
From earlier sections
V
is a countably infinite set of variables.C
a finite set of constructors.a : C -> Nat
an arity function.R : V -/-> Typ
a partial environment function.# A class to print arbitrary Sudoku-style grids, given a list of numbers | |
# Author: Ashok Menon, 01/09/2015 | |
class Array | |
def surround(delim) | |
"#{delim}#{join delim}#{delim}" | |
end | |
end | |
class Grid |