illusory0x0

///|
type Zero

///|
type Succ[N]

///|
trait Nat {}

///|

illusory0x0

struct arc {
  int32_t rc;
  uv_mutex_t mutex;
};

typedef void* moonbit_reference_t;

struct arc_ref {

illusory0x0

///|
test "split internal iterator" {
  let xs = [1, 2, 3, 4, 5]
  let iter = xs.iter().drop(4)
  inspect!(xs.iter().last(), content="Some(5)")
  inspect!(iter.head(), content="Some(5)")
}

///|
priv type ImmutExIter[A] () -> (A, ImmutExIter[A])?

illusory0x0

import Data.Function (fix)

-- lazy pattern match example
(is_odd, is_even) =
  fix
    ( \ ~(is_odd, is_even) ->
        ( (\n -> if n == 0 then False else is_even (n - 1))
        , (\n -> if n == 0 then True else is_odd (n - 1))
        )
    )

illusory0x0

Require Import Classical_Prop.
Require Import ClassicalFacts.

(* https://math.stackexchange.com/questions/447098/why-peirces-law-implies-law-of-excluded-middle *)

Definition strengthen : 
  forall P : Prop,
  (P \/ ~P -> False) -> ~P
:= 
  fun P H p => 

illusory0x0

(* https://math.stackexchange.com/questions/447098/why-peirces-law-implies-law-of-excluded-middle *)

Definition strengthen : 
  forall P : Prop,
  (P \/ ~P -> False) -> ~P
:= 
  fun P H p => 
  let e : ~P := fun p => H (or_introl p) in 
  H (or_intror e) 
.

illusory0x0

Require Import Classical_Prop.
Require Import ClassicalFacts.

Definition NNPP' : forall P:Prop, 
   excluded_middle  -> (~ ~ P -> P)
:= 
  fun P em =>
  let e1 := em P in 
  match e1 with 
    | or_intror r => fun p  => False_ind P (p r)

illusory0x0

(*

word based completion list

https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html

assumption reflexivity trivial auto discriminate exact contradiction Transforming goals

intros / intro simpl unfold apply rewrite inversion left / right replace Breaking apart goals and hypotheses

illusory0x0

(* 
 用 Gallina 重写的一个版本
  
 ref: Tactics Version 
  
 Coq里的排中律 - 遇到困难睡大觉的文章 - 知乎
 https://zhuanlan.zhihu.com/p/361454504

 *)

illusory0x0

(* https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html *)

Definition ex0 : 
  forall n : nat,
  0 = 1 -> 0 = 1 + n 
  := 
  fun n e1 => 
  nat_ind 
  (fun n => 0 = 1 + n) 
  e1