alahijani

module Euclid

import Syntax.PreorderReasoning

%default total

Divides : (divisor, dividend : Nat) -> Type
Divides d n = (q : Nat ** (n = q * d))

data Direction = LTR | RTL

TOTBWF

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}

vivshaw

If you want to see how it works, see the README on the repo.

TOTBWF

(** Core Types *)
module Syntax =
struct
  type t =
    | Local of int
    | Hole of string
    | Let of string * t * t
    | Lam of string * t
    | Ap of t * t
    | Pair of t * t

aradarbel10

{-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-}

{-
  (compiled with GHC 9.4.2)
-}

{-
  HEADS UP
  this is an example implementation of a non-trivial type system using bidirectional type checking.
  it is...