nomeata

import Lean
import Mathlib

elab "#kernel_reduce" t:term : command => Lean.Elab.Command.runTermElabM fun _ => do
  let e ← Lean.Elab.Term.elabTermAndSynthesize t none
  let e' ← Lean.ofExceptKernelException <| Lean.Kernel.whnf (← Lean.getEnv) (← Lean.getLCtx) e
  Lean.logInfo m!"{e'}"

def slow : Bool := Nat.sqrt (1000 * 1000) = 1000 

nomeata

-- This intentionally only uses std, not mathlib
import Std.Data.Array.Lemmas
import Std

set_option autoImplicit false

/-- Arrays of a given size, H'T Kyle Miller -/
def SArray (α : Type _) (n : Nat) := {a : Array α // a.size = n}

namespace SArray

nomeata

diff -ru gold0/add-adf-syn.golden gold/add-adf-syn.golden
--- gold0/add-adf-syn.golden	2022-04-07 16:58:11.733445574 +0200
+++ gold/add-adf-syn.golden	2022-04-07 16:58:22.228485530 +0200
@@ -1 +1 @@
-(addC *** coerce . coerce . curry (addC . exr)) . dup
\ No newline at end of file
+(addC *** id . repr . abst . curry (addC . exr)) . dup
\ No newline at end of file
diff -ru gold0/add-adr-syn.golden gold/add-adr-syn.golden
--- gold0/add-adr-syn.golden	2022-04-07 16:58:11.733445574 +0200

nomeata

Every now and then someone asks whether Motoko canisters can use certified variables, or whether they can serve HTTP requests with certification, and I always responded that yes, Motoko can do that, all that’s missing are a few libraries. But I figured I should put my hand where my mouth is, and actually demonstrate that it’s possible.

So here we go. If you go to https://ce7vw-haaaa-aaaai-aanva-cai.ic0.app/ you will see that

• the URL has no raw in it, so it is certified,
• that the response is actually dynamic; you can leave a message at the bottom of https://ic.rocks/principal/ce7vw-haaaa-aaaai-aanva-cai and see it show up
• this claims it’s written in Motoko.

To prove the latter claim, here is the commented code; you can also browse the full repository.

main.mo

nomeata

$ sha256sum $(nix-build -E '(import (builtins.fetchGit { url = "[email protected]:dfinity/sdk"; ref = "refs/tags/0.7.0";} + "/distributed-canisters.nix") {})')/*/*.wasm
2664385b7ad001123d8cea1f7147fad005d012116139787d9054b2f3a62718ec  /nix/store/0s2iplbgj08d32xdyjcwwyajhhg9fgzs-distributed-canisters/assetstorage/assetstorage.wasm
d6e9f851519a6dc419e3281448a84e4866fbb5011258868e2b5dda31d529bdcf  /nix/store/0s2iplbgj08d32xdyjcwwyajhhg9fgzs-distributed-canisters/ui/ui.wasm
a609400f2576d1d6df72ce868b359fd08e1d68e58454ef17db2361d2f1c242a1  /nix/store/0s2iplbgj08d32xdyjcwwyajhhg9fgzs-distributed-canisters/wallet/wallet.wasm
$ sha256sum $(nix-build -E '(import (builtins.fetchGit { url = "[email protected]:dfinity/sdk"; ref = "refs/tags/0.7.1";} + "/distributed-canisters.nix") {})')/*/*.wasm
2664385b7ad001123d8cea1f7147fad005d012116139787d9054b2f3a62718ec  /nix/store/0s2iplbgj08d32xdyjcwwyajhhg9fgzs-distributed-canisters/assetstorage/assetstorage.wasm
d6e9f851519a6dc419e3281448a84e4866fbb5011258868e2b5dda31d529bdcf  /nix/s

nomeata

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Z where
import Prelude hiding (zip)

zip :: forall a b. [a] -> [b] -> [(a,b)]
zip [] _ = []
zip _ [] = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys

nomeata

 0%  0%  0% ImplicitPrelude
 0%  0%  0% NoMonoLocalBinds
 0%  0%  0% NoRebindableSyntax
 0%  0%  0% NoMagicHash
 0%  0%  0% NoOverloadedLists
 0%  0%  0% StarIsType
 0%  1%  0% RelaxedPolyRec
 0%  4%  0% ForeignFunctionInterface
 0%  4%  0% DoAndIfThenElse
 0% 12%  0% PatternGuards

nomeata

{-# LANGUAGE TemplateHaskell #-}
module Foo where

import           Language.Haskell.TH (Q,Exp)
import qualified Language.Haskell.TH.Syntax as TH

simpleVersion :: String -> Q Exp
simpleVersion version = [|$(TH.lift version)|]

nomeata

{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE DeriveFoldable #-}

module Tree where

import Control.Monad
import Data.Maybe
import Data.Foldable

data T a = L | N (T a) a (T a) deriving (Show, Foldable)

nomeata

-- Many faces of isOrderedTree 
-- Code to the talk (extended version)

{-# LANGUAGE DeriveFoldable #-}
module Tree where

import Control.Monad
import Data.Maybe
import Data.Foldable