\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{zed-csp}
\usepackage{amsthm}
\theoremstyle{definition}
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
### 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)) |
- Install the Unity Hub
- Use the hub to install the latest LTS (long-term support) editor (e.g., 2020.3.6f1 LTS)
- No additional modules are needed during the editor install, so accept the defaults
- Use the pyenv-installer
- Update
.bashrc
:
export PYENV_ROOT="$HOME/.pyenv"