thealmarty

onePlusOne : 1+1=2
onePlusOne = Refl

thealmarty

#include <stdio.h>

void insertion(int v[], int size) {
  // invariant: the elements of v before index i are sorted
  for(int i = 1; i < size; ++i) {
    int value = v[i];
    int j = i;
    // invariant: the elements of v between j and i are sorted and > value
    for(;j > 0 && v[j-1] > value; --j) {
      v[j] = v[j-1];

thealmarty

#include <iostream>
#include <vector>

void insertion_sort(std::vector<int> & v) {
  // invariant: the first i elements of v are sorted
  for(size_t i = 1; i < v.size(); ++i) {
    int value = v[i];
    size_t j = i-1;
    // invariant: elements of v from j+1 to i inclusive are sorted and >= value
    for(; j >= 0 && v[j] > value; --j) {

thealmarty

Lessons from Idris 2

This note summarizes what Juvix can learn from the implementation of Idris 2. References:

• The paper.
• Scottish summer school 2020 slides/notes.
• Video lectures of the summer school.
• The implementation documentation.

Syntax/theory on linearity