ngrislain

-- Prompt: "Define a basic linked-list of some type α, and a dependent-type
-- SortedList that provides the proof the list is actually sorted with respect to the ordering on α."

namespace SortList

/-- A basic singly-linked list, generic over a type `α`. -/
inductive List (α : Type) where
  | nil : List α
  | cons : α → List α → List α
deriving Repr

ngrislain

-- Prompt: "Define a basic linked-list of some type α, and a dependent-type
-- SortedList that provides the proof the list is actually sorted with respect to the ordering on α."

namespace SortList

/-- A basic singly-linked list, generic over a type `α`. -/
inductive List (α : Type) where
  | nil : List α
  | cons : α → List α → List α
deriving Repr

ngrislain

import pyxel

WIDTH = 640
HEIGHT = 400
FOCUS = 200
TRANSPARENT_COLOR = 1
BACKGROUND_COLOR = 0
SKY_COLOR = 1
GROUND_COLOR = 3
TEXT_COLOR = 7

ngrislain

ngrislain

docker run --rm -it -v $(pwd):/repository python:3.7 /bin/bash