AlecsFerra
/ map_inj_free_groups.lean
Created
March 13, 2026 10:08
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib | |
| import Mathlib.Algebra.Group.Pi.Basic | |
| import Mathlib.Algebra.Group.Subgroup.Ker | |
| import Mathlib.Data.List.Chain | |
| import Mathlib.Algebra.Group.Int.Defs | |
| import Mathlib.Algebra.BigOperators.Group.List.Defs | |
| namespace FreeGroup |
AlecsFerra
/ install.sh
Created
February 10, 2026 10:08
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #! /usr/bin/env bash | |
| DIRS=( | |
| "liquid-prelude" | |
| "liquid-parallel" | |
| "liquid-vector" | |
| "." # This must be the last entry | |
| ) | |
| echo "Installing libraries globally..." |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| theory Scratch | |
| imports ZF | |
| begin | |
| consts ty :: "i" | |
| datatype "ty" | |
| = TyNat | |
| | TyBool | |
| | TyArr ("τ ∈ ty", "υ ∈ ty") |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--ple" @-} | |
| module Rotate where | |
| import Language.Haskell.Liquid.ProofCombinators | |
| {-@ measure length' @-} | |
| {-@ length' :: [a] -> Nat @-} | |
| length' :: [a] -> Int |
AlecsFerra
/ MM.hs
Created
January 29, 2025 10:17
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS_GHC -fplugin=LiquidHaskell #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE LambdaCase #-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--etabeta" @-} | |
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--save" @-} | |
| {-@ LIQUID "--dependantcase" @-} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--etabeta" @-} | |
| module State where | |
| import Language.Haskell.Liquid.ProofCombinators | |
| import Prelude hiding (return, (>>=)) | |
| data Pair a b = MkPair a b |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE LambdaCase #-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--etabeta" @-} | |
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--dependantcase" @-} | |
| module ExprCompiler where |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--etabeta" @-} | |
| module CTC where | |
| import Prelude hiding (id) | |
| import Language.Haskell.Liquid.ProofCombinators | |
| data Cat k = Cat |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE RankNTypes #-} | |
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--etabeta" @-} | |
| {-@ LIQUID "--save" @-} | |
| module FuseMap where | |
| import Prelude hiding (map, foldr) | |
| import Language.Haskell.Liquid.ProofCombinators |
AlecsFerra
/ Langs.hs
Created
November 29, 2024 12:11
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS_GHC -fplugin=LiquidHaskell #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-@ LIQUID "--reflection" @-} | |
| {-@ LIQUID "--ple" @-} | |
| {-@ LIQUID "--etabeta" @-} | |
| {-@ LIQUID "--dependantcase" @-} | |
| {-@ LIQUID "--max-case-expand=4" @-} | |
| module Langs where |
NewerOlder