tmoux

import Mathlib.Util.AtomM
import Mathlib.Data.Nat.Basic

open Lean Elab Meta Tactic Mathlib.Tactic
open Lean.Expr

namespace Monoid
structure Context where
  α : Expr -- The type of the expression
  univ : Level -- The universe level of α

tmoux

import Mathlib.Util.AtomM
import Mathlib.Data.Nat.Basic

open Lean Elab Meta Tactic Mathlib.Tactic
open Lean.Expr

-- Monoid simplifier tactic
-- Normalize expressions by flattening to a list of atoms and eliminating identity elements.

namespace Monoid

tmoux

{-# LANGUAGE TemplateHaskell #-}
module Main where

import Term
import TH

idf :: Term Ty
idf = $$(typecheck (lam "x" Base (var "x")))

-- Invalid: unbound variable

tmoux

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Rewriting.P where

tmoux

(*|
==========================================
Verifying Programming Contest Problems
==========================================

In programming contests, one of the most frustrating (and common!) verdicts to receive is Wrong Answer (WA).
One of the reasons behind this is that there are often many potential sources of WA that a programmer has to hunt down.
A WA could come from a typo in the implementation, or it could come from the use of a greedy algorithm which is not always correct, or many other reasons.

In this tutorial, I will try to give a brief overview of how you can *prove your programs correct* by writing specifications and proofs in the Coq proof assistant.

tmoux

Require Import Unicode.Utf8.
Require Import Relations.Relation_Operators.
Require Import List.
Require Import Autosubst.Autosubst.

(* We present a simple proof of type safety for STLC using logical relations.
   We use the Autosubst library to handle binding/substitutions.
   It also makes it easy to state and prove details about substitutions in the fundamental lemma. *)

Inductive type : Type :=

tmoux

module Mwe where

open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)

data Type : Set where
  ⊤ : Type
  _⇒_ : Type → Type → Type
infix 30 _⇒_

data Context : Set where

tmoux

(** val add : int64 -> int64 -> int64 **)

let rec add = Int64.add

(** val mul : int64 -> int64 -> int64 **)

let rec mul = Int64.mul

module Nat =
 struct

tmoux

name C {z =>
  type R <= Int
}

name D {z =>
  type R <= Top 
}
subtype D {type R <= Int} <: C
//D is some conditional subtype of C