Skip to content

Instantly share code, notes, and snippets.

View Russoul's full-sized avatar

Ruslan Φ. Russoul

39 followers · 4 following
  • Tbilisi, Georgia
View GitHub Profile
@Russoul
Russoul / ToS.txt
Created July 5, 2024 12:21
Simple extrinsically typed signatures with two universes (one included in another)
------------ SYNTAX -------------
Γ ::= ε | Γ (x : A)
A, B, f, e ::= Sort | Sort₁ | x | f e | (x : A) → B
------------ JUDGEMENT FORMS -------------
Γ con
@Russoul
Russoul / DepPath.idr
Last active August 7, 2023 02:09
Dependent rewriting
module Data.DepPath
import Data.Nat
import Data.Vect
||| Equivalent to the built-in `replace`.
public export
transport1 : (0 a0 : Type)
-> (0 a1 : a0 -> Type)
-> (0 x0 : a0)
@Russoul
Russoul / dependent-mult-map.idr
Last active May 8, 2021 20:56
%default total
data Use = None | Once | Many
%hide Prelude.Num.(*)
%hide Prelude.Num.(+)
%hide Prelude.List
%hide Prelude.(::)
%hide Prelude.Nil
%hide Prelude.map
@Russoul
Russoul / Typesafe.idr
Created November 7, 2020 15:22
Type-safe foreign values in Idris 2
-- NOT A SELF-SUSTAINED EXAMPLE, WON'T RUN ON ITS OWN.
||| Any Lua value marked with a label, basically we assign a type to it.
export
data Typed : (label : a) -> Type where [external]
||| A proof that the given typed value is a table with an assessible key `field` holding a value of type `return`
||| Users can't normally build this proof term.
export
@Russoul
Russoul / Test.idr
Last active September 23, 2020 07:51
(Rough) Translation of interfaces to data and function definitions
-- interface A x where
-- constructor MkA
-- methodA : x
-- interface A x => B x where
-- constructor MkB
-- methodB : x
-- A Bool where
-- methodA = True