Python
Setup
pyenv
- Use the pyenv-installer
- Update
.bashrc
:
export PYENV_ROOT="$HOME/.pyenv"
.bashrc
:export PYENV_ROOT="$HOME/.pyenv"
### A Pluto.jl notebook ### | |
# v0.12.3 | |
using Markdown | |
using InteractiveUtils | |
# This Pluto notebook uses @bind for interactivity. When running this notebook outside of Pluto, the following 'mock version' of @bind gives bound variables a default value (instead of an error). | |
macro bind(def, element) | |
quote | |
local el = $(esc(element)) |
data Foo a = Bar a | |
| Baz (Foo a) (Foo a) | |
fooEq : DecEq a => a -> a -> Foo a -> Foo a -> Maybe (Foo a) | |
fooEq x y f g = case decEq x y of | |
Yes _ => Just (Baz f g) | |
No _ => Nothing | |
comb : DecEq a => Foo a -> Foo a -> Maybe (Foo a) | |
comb f@(Bar x ) g@(Bar y ) = fooEq x y f g -- < ok |
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{zed-csp}
\usepackage{amsthm}
\theoremstyle{definition}
data Foo : (x : List a) -> (y : List b) -> Type where | |
MkFoo : (bar: a -> b) -> Foo x y | |
bar : Foo {a} {b} x y -> a -> b | |
bar (MkFoo _) x' = ?rhs | |
{- | |
b : Type | |
a : Type | |
y : List b |
record Foo where | |
constructor MkFoo | |
from : Type | |
to : Type | |
bar : (a : Foo) -> (x : from a) -> (to a) | |
-- impl not important | |
baz : (a : Foo) -> (b : Foo) -> ((to b) = (from a)) => (x: from b) -> (to a) |